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

Theorem syl5bbr 192
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 130 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 190 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3bitr3g  220  ianordc  833  19.16  1488  19.19  1597  cbvab  2202  necon1bbiidc  2307  rspc2gv  2713  elabgt  2736  sbceq1a  2825  sbcralt  2891  sbcrext  2892  sbccsbg  2935  sbccsb2g  2936  iunpw  4237  tfis  4332  xp11m  4789  ressn  4888  fnssresb  5042  fun11iun  5178  funimass4  5256  dffo4  5347  f1ompt  5352  fliftf  5470  resoprab2  5629  ralrnmpt2  5646  rexrnmpt2  5647  1stconst  5873  2ndconst  5874  dfsmo2  5936  smoiso  5951  brecop  6262  ac6sfi  6431  prarloclemn  6751  axcaucvglemres  7127  reapti  7746  indstr  8762  iccneg  9087  sqap0  9639  sqrt00  10064  prmind2  10646
  Copyright terms: Public domain W3C validator