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

Theorem syl5rbbr 260
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 202 . 2  |-  ( ph  <->  ps )
3 syl5rbbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5rbb 258 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  sbco3  2137  sbco3OLD  2138  sbal2OLD  2206  necon2bbid  2723  fressnfv  6075  eluniima  6150  dfac2  8511  alephval2  8947  adderpqlem  9332  1idpr  9407  leloe  9671  negeq0  9873  muleqadd  10193  addltmul  10774  xrleloe  11350  fzrev  11742  mod0  11971  modirr  12025  cjne0  12959  lenegsq  13116  fsumsplit  13525  sumsplit  13546  xpsfrnel  14818  isacs2  14908  acsfn  14914  comfeq  14962  resscntz  16174  gexdvds  16410  hauscmplem  19700  hausdiag  19909  utop3cls  20517  ltgov  23738  colinearalglem2  23914  ax5seglem4  23939  mdsl2i  26945  addeq0  27258  pl1cn  27601  ghomfo  28534  ftc1anclem5  29699  fdc1  29870  stoweidlem28  31356  e2ebind  32434  lcvexchlem1  33849  lkreqN  33985  glbconxN  34192  islpln5  34349  islvol5  34393  cdlemefrs29bpre0  35210  cdlemg17h  35482  cdlemg33b  35521
  Copyright terms: Public domain W3C validator