ILE Home 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  |-  ( ps  <->  ph )
syl5bbr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5bbr  |-  ( ch 
->  ( ph  <->  th )
)

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3  |-  ( ps  <->  ph )
21bicomi 131 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 191 1  |-  ( ch 
->  ( ph  <->  th )
)
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  869  19.16  1519  19.19  1629  cbvab  2240  necon1bbiidc  2346  rspc2gv  2775  elabgt  2799  sbceq1a  2891  sbcralt  2957  sbcrext  2958  sbccsbg  3001  sbccsb2g  3002  iunpw  4371  tfis  4467  xp11m  4947  ressn  5049  fnssresb  5205  fun11iun  5356  funimass4  5440  dffo4  5536  f1ompt  5539  fliftf  5668  resoprab2  5836  ralrnmpo  5853  rexrnmpo  5854  1stconst  6086  2ndconst  6087  dfsmo2  6152  smoiso  6167  brecop  6487  ixpsnf1o  6598  ac6sfi  6760  ismkvnex  6997  prarloclemn  7275  axcaucvglemres  7675  reapti  8309  indstr  9356  iccneg  9740  sqap0  10327  sqrt00  10780  minclpr  10976  absefib  11404  efieq1re  11405  prmind2  11728  sincosq3sgn  12836  sincosq4sgn  12837
  Copyright terms: Public domain W3C validator