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

Theorem syl5rbbr 194
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 131 . 2  |-  ( ph  <->  ps )
3 syl5rbbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5rbb 192 1  |-  ( ch 
->  ( th  <->  ph ) )
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:  xordc  1355  sbal2  1975  eqsnm  3652  fnressn  5574  fressnfv  5575  eluniimadm  5634  genpassl  7300  genpassu  7301  1idprl  7366  1idpru  7367  axcaucvglemres  7675  negeq0  7984  muleqadd  8396  crap0  8680  addltmul  8914  fzrev  9819  modq0  10057  cjap0  10634  cjne0  10635  caucvgrelemrec  10706  lenegsq  10822  isumss  11115  fsumsplit  11131  sumsplitdc  11156  dvdsabseq  11457  oddennn  11816  metrest  12586  elabgf0  12880
  Copyright terms: Public domain W3C validator