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

Theorem syl5rbbr 252
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 194 . 2  |-  ( ph  <->  ps )
3 syl5rbbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5rbb 250 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  sbco3  2122  sbal2  2169  fressnfv  5860  eluniima  5937  dfac2  7945  alephval2  8381  adderpqlem  8765  1idpr  8840  leloe  9095  negeq0  9288  muleqadd  9599  addltmul  10136  xrleloe  10670  fzrev  11040  mod0  11183  modirr  11214  cjne0  11896  lenegsq  12052  fsumsplit  12461  sumsplit  12480  xpsfrnel  13716  isacs2  13806  acsfn  13812  comfeq  13860  resscntz  15058  gexdvds  15146  hauscmplem  17392  hausdiag  17599  utop3cls  18203  mdsl2i  23674  addeq0  23956  ghomfo  24882  colinearalglem2  25561  ax5seglem4  25586  fdc1  26142  stoweidlem28  27446  e2ebind  27994  sbco3wAUX7  28923  sbco3OLD7  29071  sbal2OLD7  29086  lcvexchlem1  29150  lkreqN  29286  glbconxN  29493  islpln5  29650  islvol5  29694  cdlemefrs29bpre0  30511  cdlemg17h  30783  cdlemg33b  30822
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 178
  Copyright terms: Public domain W3C validator