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  835  19.16  1490  19.19  1599  cbvab  2207  necon1bbiidc  2312  rspc2gv  2725  elabgt  2748  sbceq1a  2838  sbcralt  2904  sbcrext  2905  sbccsbg  2948  sbccsb2g  2949  iunpw  4274  tfis  4370  xp11m  4832  ressn  4934  fnssresb  5088  fun11iun  5231  funimass4  5312  dffo4  5404  f1ompt  5407  fliftf  5533  resoprab2  5693  ralrnmpt2  5710  rexrnmpt2  5711  1stconst  5937  2ndconst  5938  dfsmo2  6000  smoiso  6015  brecop  6328  ac6sfi  6560  prarloclemn  6995  axcaucvglemres  7371  reapti  7990  indstr  9006  iccneg  9331  sqap0  9912  sqrt00  10361  prmind2  10969
  Copyright terms: Public domain W3C validator