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

Theorem syl5bbr 187
 Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bbr.1 (𝜓𝜑)
syl5bbr.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bbr (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3 (𝜓𝜑)
21bicomi 127 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 185 1 (𝜒 → (𝜑𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  3bitr3g  215  ianordc  810  19.16  1463  19.19  1572  cbvab  2176  necon1bbiidc  2281  rspc2gv  2684  elabgt  2707  sbceq1a  2796  sbcralt  2862  sbcrext  2863  sbccsbg  2906  sbccsb2g  2907  iunpw  4239  tfis  4334  xp11m  4787  ressn  4886  fnssresb  5039  fun11iun  5175  funimass4  5252  dffo4  5343  f1ompt  5348  fliftf  5467  resoprab2  5626  ralrnmpt2  5643  rexrnmpt2  5644  1stconst  5870  2ndconst  5871  dfsmo2  5933  smoiso  5948  brecop  6227  ac6sfi  6383  prarloclemn  6655  axcaucvglemres  7031  reapti  7644  indstr  8632  iccneg  8958  sqap0  9486  sqrt00  9867
 Copyright terms: Public domain W3C validator