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

Theorem syl5rbbr 193
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl5rbbr.1  |-  ( ps  <->  ph )
syl5rbbr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5rbbr  |-  ( ch 
->  ( th  <->  ph ) )

Proof of Theorem syl5rbbr
StepHypRef Expression
1 syl5rbbr.1 . . 3  |-  ( ps  <->  ph )
21bicomi 130 . 2  |-  ( ph  <->  ps )
3 syl5rbbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5rbb 191 1  |-  ( ch 
->  ( th  <->  ph ) )
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:  xordc  1324  sbal2  1940  eqsnm  3555  fnressn  5381  fressnfv  5382  eluniimadm  5436  genpassl  6776  genpassu  6777  1idprl  6842  1idpru  6843  axcaucvglemres  7127  negeq0  7429  muleqadd  7825  crap0  8102  addltmul  8334  fzrev  9177  modq0  9411  cjap0  9932  cjne0  9933  caucvgrelemrec  10003  lenegsq  10119  dvdsabseq  10392  oddennn  10730  elabgf0  10765
  Copyright terms: Public domain W3C validator