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  1353  sbal2  1973  eqsnm  3650  fnressn  5572  fressnfv  5573  eluniimadm  5632  genpassl  7296  genpassu  7297  1idprl  7362  1idpru  7363  axcaucvglemres  7671  negeq0  7980  muleqadd  8392  crap0  8676  addltmul  8910  fzrev  9815  modq0  10053  cjap0  10630  cjne0  10631  caucvgrelemrec  10702  lenegsq  10818  isumss  11111  fsumsplit  11127  sumsplitdc  11152  dvdsabseq  11452  oddennn  11811  metrest  12581  elabgf0  12818
  Copyright terms: Public domain W3C validator