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

Theorem syl5rbbr 263
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 205 . 2  |-  ( ph  <->  ps )
3 syl5rbbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5rbb 261 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  sbco3  2212  necon2bbid  2687  fressnfv  6093  eluniima  6170  dfac2  8559  alephval2  8995  adderpqlem  9378  1idpr  9453  leloe  9719  negeq0  9927  muleqadd  10255  addltmul  10848  xrleloe  11443  fzrev  11856  mod0  12100  modirr  12157  cjne0  13205  lenegsq  13362  fsumsplit  13784  sumsplit  13807  xpsfrnel  15424  isacs2  15514  acsfn  15520  comfeq  15566  sgrp2nmndlem3  16614  resscntz  16940  gexdvds  17175  hauscmplem  20356  hausdiag  20595  utop3cls  21201  ltgov  24510  colinearalglem2  24791  ax5seglem4  24816  mdsl2i  27818  addeq0  28171  pl1cn  28608  ghomfo  30105  topdifinfeq  31495  ftc1anclem5  31736  fdc1  31790  lcvexchlem1  32320  lkreqN  32456  glbconxN  32663  islpln5  32820  islvol5  32864  cdlemefrs29bpre0  33683  cdlemg17h  33955  cdlemg33b  33994  frege92  36203  e2ebind  36582  stoweidlem28  37472
  Copyright terms: Public domain W3C validator