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

Theorem syl6rbb 254
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 253 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 193 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl6rbbr  256  bibif  336  pm5.61  694  oranabs  830  necon4bid  2633  resopab2  5149  xpco  5373  funconstss  5807  xpopth  6347  map1  7144  ac6sfi  7310  rankr1bg  7685  alephsdom  7923  brdom7disj  8365  fpwwe2lem13  8473  nn0sub  10226  elznn0  10252  supxrbnd1  10856  supxrbnd2  10857  rexuz3  12107  smueqlem  12957  qnumdenbi  13091  lssne0  15982  pjfval2  16891  0top  17003  1stccn  17479  dscopn  18574  bcthlem1  19230  ovolgelb  19329  iblpos  19637  itgposval  19640  itgsubstlem  19885  sincosq3sgn  20361  sincosq4sgn  20362  lgsquadlem3  21093  nmoo0  22245  leop3  23581  leoptri  23592  tltnle  24143  nofulllem5  25574  dfrdg4  25703  colinearalg  25753  itgaddnclem2  26163  lzunuz  26716  2reu4a  27834  funressnfv  27859  usgreg2spot  28170  lfl1dim  29604  glbconxN  29860  2dim  29952  elpadd0  30291  dalawlem13  30365  diclspsn  31677  dihglb2  31825  dochsordN  31857
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