MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5rbbr Structured version   Unicode version

Theorem syl5rbbr 253
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 195 . 2  |-  ( ph  <->  ps )
3 syl5rbbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5rbb 251 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  sbco3  2169  sbal2  2217  fressnfv  5949  eluniima  6026  dfac2  8042  alephval2  8478  adderpqlem  8862  1idpr  8937  leloe  9192  negeq0  9386  muleqadd  9697  addltmul  10234  xrleloe  10768  fzrev  11139  mod0  11286  modirr  11317  cjne0  11999  lenegsq  12155  fsumsplit  12564  sumsplit  12583  xpsfrnel  13819  isacs2  13909  acsfn  13915  comfeq  13963  resscntz  15161  gexdvds  15249  hauscmplem  17500  hausdiag  17708  utop3cls  18312  mdsl2i  23856  addeq0  24145  ghomfo  25133  colinearalglem2  25877  ax5seglem4  25902  ftc1anclem5  26322  fdc1  26488  stoweidlem28  27791  e2ebind  28748  sbco3wAUX7  29685  sbco3OLD7  29852  sbal2OLD7  29866  lcvexchlem1  29930  lkreqN  30066  glbconxN  30273  islpln5  30430  islvol5  30474  cdlemefrs29bpre0  31291  cdlemg17h  31563  cdlemg33b  31602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator