Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2anb GIF version

Theorem syl2anb 275
 Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
Hypotheses
Ref Expression
syl2anb.1 (𝜑𝜓)
syl2anb.2 (𝜏𝜒)
syl2anb.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
syl2anb ((𝜑𝜏) → 𝜃)

Proof of Theorem syl2anb
StepHypRef Expression
1 syl2anb.2 . 2 (𝜏𝜒)
2 syl2anb.1 . . 3 (𝜑𝜓)
3 syl2anb.3 . . 3 ((𝜓𝜒) → 𝜃)
42, 3sylanb 268 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 271 1 ((𝜑𝜏) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  sylancb  395  reupick3  3222  difprsnss  3502  trin2  4716  imadiflem  4978  fnun  5005  fco  5056  f1co  5101  foco  5116  f1oun  5146  f1oco  5149  eqfunfv  5270  ftpg  5347  issmo  5903  tfrlem5  5930  ener  6259  domtr  6265  unen  6293  xpdom2  6305  axpre-lttrn  6958  axpre-mulgt0  6961  zmulcl  8297  qaddcl  8570  qmulcl  8572  rpaddcl  8606  rpmulcl  8607  rpdivcl  8608  xrltnsym  8714  xrlttri3  8718  ge0addcl  8850  ge0mulcl  8851  serige0  9252  expclzaplem  9279  expge0  9291  expge1  9292
 Copyright terms: Public domain W3C validator