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

Theorem syl6rbb 262
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 261 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 201 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  syl6rbbr  264  bibif  346  pm5.61  705  oranabs  845  necon4bid  2667  resopab2  5143  xpco  5365  funconstss  5809  xpopth  6604  map1  7376  ac6sfi  7544  rankr1bg  7998  alephsdom  8244  brdom7disj  8686  fpwwe2lem13  8796  nn0sub  10617  elznn0  10648  supxrbnd1  11271  supxrbnd2  11272  rexuz3  12819  smueqlem  13668  qnumdenbi  13804  lssne0  16953  pjfval2  17975  0top  18429  1stccn  18908  dscopn  20007  bcthlem1  20676  ovolgelb  20804  iblpos  21111  itgposval  21114  itgsubstlem  21361  sincosq3sgn  21846  sincosq4sgn  21847  lgsquadlem3  22579  colinearalg  22978  nmoo0  24013  leop3  25351  leoptri  25362  f1od2  25847  tltnle  25945  nofulllem5  27693  dfrdg4  27827  itgaddnclem2  28292  lzunuz  28948  2reu4a  29856  funressnfv  29877  nn01to3  30030  wlklniswwlkn2  30177  rusgranumwlkb0  30414  usgreg2spot  30503  extwwlkfab  30526  numclwwlk2lem1  30538  lfl1dim  32336  glbconxN  32592  2dim  32684  elpadd0  33023  dalawlem13  33097  diclspsn  34409  dihglb2  34557  dochsordN  34589
  Copyright terms: Public domain W3C validator