Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5bbr Unicode 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-1 5  ax-2 6  ax-mp 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  865  19.16  1515  19.19  1625  cbvab  2235  necon1bbiidc  2341  rspc2gv  2769  elabgt  2793  sbceq1a  2885  sbcralt  2951  sbcrext  2952  sbccsbg  2995  sbccsb2g  2996  iunpw  4359  tfis  4455  xp11m  4933  ressn  5035  fnssresb  5191  fun11iun  5342  funimass4  5424  dffo4  5520  f1ompt  5523  fliftf  5652  resoprab2  5820  ralrnmpo  5837  rexrnmpo  5838  1stconst  6070  2ndconst  6071  dfsmo2  6136  smoiso  6151  brecop  6471  ixpsnf1o  6582  ac6sfi  6743  prarloclemn  7249  axcaucvglemres  7628  reapti  8253  indstr  9284  iccneg  9659  sqap0  10246  sqrt00  10698  minclpr  10894  absefib  11321  efieq1re  11322  prmind2  11641
 Copyright terms: Public domain W3C validator