MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5rbbr Structured version   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  2163  sbal2  2210  fressnfv  5912  eluniima  5989  dfac2  8003  alephval2  8439  adderpqlem  8823  1idpr  8898  leloe  9153  negeq0  9347  muleqadd  9658  addltmul  10195  xrleloe  10729  fzrev  11100  mod0  11247  modirr  11278  cjne0  11960  lenegsq  12116  fsumsplit  12525  sumsplit  12544  xpsfrnel  13780  isacs2  13870  acsfn  13876  comfeq  13924  resscntz  15122  gexdvds  15210  hauscmplem  17461  hausdiag  17669  utop3cls  18273  mdsl2i  23817  addeq0  24106  ghomfo  25094  colinearalglem2  25838  ax5seglem4  25863  ftc1anclem5  26274  fdc1  26441  stoweidlem28  27744  e2ebind  28587  sbco3wAUX7  29524  sbco3OLD7  29691  sbal2OLD7  29705  lcvexchlem1  29769  lkreqN  29905  glbconxN  30112  islpln5  30269  islvol5  30313  cdlemefrs29bpre0  31130  cdlemg17h  31402  cdlemg33b  31441
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