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

Theorem syl5bbr 193
 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 131 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 191 1 (𝜒 → (𝜑𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  3bitr3g  221  ianordc  867  19.16  1517  19.19  1627  cbvab  2238  necon1bbiidc  2344  rspc2gv  2773  elabgt  2797  sbceq1a  2889  sbcralt  2955  sbcrext  2956  sbccsbg  2999  sbccsb2g  3000  iunpw  4369  tfis  4465  xp11m  4945  ressn  5047  fnssresb  5203  fun11iun  5354  funimass4  5438  dffo4  5534  f1ompt  5537  fliftf  5666  resoprab2  5834  ralrnmpo  5851  rexrnmpo  5852  1stconst  6084  2ndconst  6085  dfsmo2  6150  smoiso  6165  brecop  6485  ixpsnf1o  6596  ac6sfi  6758  ismkvnex  6995  prarloclemn  7271  axcaucvglemres  7671  reapti  8304  indstr  9340  iccneg  9723  sqap0  10310  sqrt00  10763  minclpr  10959  absefib  11386  efieq1re  11387  prmind2  11708
 Copyright terms: Public domain W3C validator