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  2114  sbco3OLD  2115  sbal2OLD  2184  fressnfv  5894  eluniima  5965  dfac2  8298  alephval2  8734  adderpqlem  9121  1idpr  9196  leloe  9459  negeq0  9661  muleqadd  9978  addltmul  10558  xrleloe  11119  fzrev  11517  mod0  11713  modirr  11767  cjne0  12650  lenegsq  12806  fsumsplit  13214  sumsplit  13233  xpsfrnel  14499  isacs2  14589  acsfn  14595  comfeq  14643  resscntz  15847  gexdvds  16081  hauscmplem  19007  hausdiag  19216  utop3cls  19824  colinearalglem2  23151  ax5seglem4  23176  mdsl2i  25724  addeq0  26033  pl1cn  26383  ghomfo  27308  ftc1anclem5  28468  fdc1  28639  stoweidlem28  29820  e2ebind  31269  lcvexchlem1  32676  lkreqN  32812  glbconxN  33019  islpln5  33176  islvol5  33220  cdlemefrs29bpre0  34037  cdlemg17h  34309  cdlemg33b  34348
  Copyright terms: Public domain W3C validator