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

Theorem syl5rbbr 251
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 193 . 2  |-  ( ph  <->  ps )
3 syl5rbbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5rbb 249 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  sbco3  2028  sbal2  2073  fressnfv  5707  eluniima  5776  dfac2  7757  alephval2  8194  adderpqlem  8578  1idpr  8653  leloe  8908  negeq0  9101  muleqadd  9412  addltmul  9947  xrleloe  10478  fzrev  10846  mod0  10978  modirr  11009  cjne0  11648  lenegsq  11804  fsumsplit  12212  sumsplit  12231  xpsfrnel  13465  isacs2  13555  acsfn  13561  comfeq  13609  resscntz  14807  gexdvds  14895  hauscmplem  17133  mdsl2i  22902  addeq0  23043  ghomfo  23998  colinearalglem2  24535  ax5seglem4  24560  fdc1  26456  stoweidlem28  27777  e2ebind  28329  lcvexchlem1  29224  lkreqN  29360  glbconxN  29567  islpln5  29724  islvol5  29768  cdlemefrs29bpre0  30585  cdlemg17h  30857  cdlemg33b  30896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator