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

Theorem syl5rbbr 184
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 123 . 2  |-  ( ph  <->  ps )
3 syl5rbbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5rbb 182 1  |-  ( ch 
->  ( th  <->  ph ) )
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:  xordc  1283  sbal2  1898  eqsnm  3526  fnressn  5349  fressnfv  5350  eluniimadm  5404  genpassl  6622  genpassu  6623  1idprl  6688  1idpru  6689  axcaucvglemres  6973  negeq0  7265  muleqadd  7649  crap0  7910  addltmul  8161  fzrev  8946  modq0  9171  cjap0  9507  cjne0  9508  caucvgrelemrec  9578  lenegsq  9691  elabgf0  9916
  Copyright terms: Public domain W3C validator