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

Theorem syl5rbbr 251
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 193 . 2  |-  ( ph  <->  ps )
3 syl5rbbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5rbb 249 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  sbco3  2041  sbal2  2086  fressnfv  5723  eluniima  5792  dfac2  7773  alephval2  8210  adderpqlem  8594  1idpr  8669  leloe  8924  negeq0  9117  muleqadd  9428  addltmul  9963  xrleloe  10494  fzrev  10862  mod0  10994  modirr  11025  cjne0  11664  lenegsq  11820  fsumsplit  12228  sumsplit  12247  xpsfrnel  13481  isacs2  13571  acsfn  13577  comfeq  13625  resscntz  14823  gexdvds  14911  hauscmplem  17149  mdsl2i  22918  addeq0  23059  ghomfo  24013  colinearalglem2  24607  ax5seglem4  24632  fdc1  26559  stoweidlem28  27880  e2ebind  28628  sbco3wAUX7  29561  sbco3OLD7  29708  sbal2OLD7  29724  lcvexchlem1  29846  lkreqN  29982  glbconxN  30189  islpln5  30346  islvol5  30390  cdlemefrs29bpre0  31207  cdlemg17h  31479  cdlemg33b  31518
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 177
  Copyright terms: Public domain W3C validator