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

Theorem syl5bbr 183
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 123 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 181 1  |-  ( ch 
->  ( ph  <->  th )
)
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  6595  axcaucvglemres  6971  reapti  7568  indstr  8534  iccneg  8855  sqap0  9294  sqrt00  9612
  Copyright terms: Public domain W3C validator