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  2525  resopab2  5015  funconstss  5659  xpopth  6177  map1  6955  ac6sfi  7117  rankr1bg  7491  alephsdom  7729  brdom7disj  8172  fpwwe2lem13  8280  nn0sub  10030  elznn0  10054  supxrbnd1  10656  supxrbnd2  10657  rexuz3  11848  smueqlem  12697  qnumdenbi  12831  lssne0  15724  pjfval2  16625  0top  16737  1stccn  17205  dscopn  18112  bcthlem1  18762  ovolgelb  18855  iblpos  19163  itgposval  19166  itgsubstlem  19411  sincosq3sgn  19884  sincosq4sgn  19885  lgsquadlem3  20611  nmoo0  21385  leop3  22721  leoptri  22732  nofulllem5  24431  dfrdg4  24560  colinearalg  24610  lzunuz  26950  2reu4a  28070  funressnfv  28096  lfl1dim  29933  glbconxN  30189  2dim  30281  elpadd0  30620  dalawlem13  30694  diclspsn  32006  dihglb2  32154  dochsordN  32186
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