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

Theorem syl5bbr 183
 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 123 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 181 1 (𝜒 → (𝜑𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ 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:  3bitr3g  211  ianordc  799  19.16  1447  19.19  1556  cbvab  2160  necon1bbiidc  2266  elabgt  2684  sbceq1a  2773  sbcralt  2834  sbcrext  2835  sbccsbg  2878  sbccsb2g  2879  iunpw  4211  tfis  4306  xp11m  4759  ressn  4858  fnssresb  5011  fun11iun  5147  funimass4  5224  dffo4  5315  f1ompt  5320  fliftf  5439  resoprab2  5598  ralrnmpt2  5615  rexrnmpt2  5616  1stconst  5842  2ndconst  5843  dfsmo2  5902  smoiso  5917  brecop  6196  ac6sfi  6352  prarloclemn  6597  axcaucvglemres  6973  reapti  7570  indstr  8536  iccneg  8857  sqap0  9320  sqrt00  9638
 Copyright terms: Public domain W3C validator