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

Theorem syl6rbb 253
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6rbb.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6rbb.2  |-  ( ch  <->  th )
Assertion
Ref Expression
syl6rbb  |-  ( ph  ->  ( th  <->  ps )
)

Proof of Theorem syl6rbb
StepHypRef Expression
1 syl6rbb.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6rbb.2 . . 3  |-  ( ch  <->  th )
31, 2syl6bb 252 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 192 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  syl6rbbr  255  bibif  335  pm5.61  693  oranabs  829  necon4bid  2512  resopab2  4999  funconstss  5643  xpopth  6161  map1  6939  ac6sfi  7101  rankr1bg  7475  alephsdom  7713  brdom7disj  8156  fpwwe2lem13  8264  nn0sub  10014  elznn0  10038  supxrbnd1  10640  supxrbnd2  10641  rexuz3  11832  smueqlem  12681  qnumdenbi  12815  lssne0  15708  pjfval2  16609  0top  16721  1stccn  17189  dscopn  18096  bcthlem1  18746  ovolgelb  18839  iblpos  19147  itgposval  19150  itgsubstlem  19395  sincosq3sgn  19868  sincosq4sgn  19869  lgsquadlem3  20595  nmoo0  21369  leop3  22705  leoptri  22716  nofulllem5  24360  dfrdg4  24488  colinearalg  24538  lzunuz  26847  2reu4a  27967  funressnfv  27991  lfl1dim  29311  glbconxN  29567  2dim  29659  elpadd0  29998  dalawlem13  30072  diclspsn  31384  dihglb2  31532  dochsordN  31564
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