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

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

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3  |-  ( ps  <->  ph )
21bicomi 202 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 257 1  |-  ( ch 
->  ( ph  <->  th )
)
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:  3bitr3g  287  biass  359  19.16  1904  19.19  1906  sbco2OLD  2135  sbcom2  2173  sbal2  2195  cbvabOLD  2609  necon1bbid  2717  necon4abidOLD  2719  elabgt  3247  sbceq1a  3342  sbcralt  3412  sbccsbgOLD  3850  sbccsb2  3851  sbccsb2gOLD  3852  disjxun  4445  xp11  5442  ressn  5543  fnssresb  5693  dmfco  5941  dffo4  6037  f1ompt  6043  funressn  6074  fnsuppeq0OLD  6122  elunirnALT  6152  fliftf  6201  resoprab2  6383  elrnmpt2res  6400  ralrnmpt2  6401  iunpw  6598  ordunisuc2  6663  tfis  6673  tfinds  6678  dfom2  6686  fun11iun  6744  opiota  6843  1stconst  6871  2ndconst  6872  fnsuppeq0  6928  iinon  7011  dfsmo2  7018  oeeui  7251  omabs  7296  brecop  7404  ixpsnf1o  7509  boxcutc  7512  ac6sfi  7764  wemapwe  8139  wemapweOLD  8140  sdom2en01  8682  ac6num  8859  zorn2lem7  8882  ttukeylem6  8894  alephval2  8947  fpwwe2  9021  fpwwe  9024  nqereu  9307  suplem2pr  9431  map2psrpr  9487  supsrlem  9488  fimaxre3  10492  infm3  10502  crne0  10529  nn1suc  10557  uzindOLD  10955  xmulneg1  11461  supxrbnd1  11513  supxrbnd2  11514  iccneg  11641  wrdind  12665  cnpart  13036  sqrt00  13060  lo1resb  13350  o1resb  13352  absefib  13794  efieq1re  13795  sadadd2lem2  13959  saddisjlem  13973  prmind2  14087  mreacs  14913  issubc  15065  isfunc  15091  pospo  15460  mrcmndind  15816  eqgval  16055  resscntz  16174  frgpuplem  16596  divsabl  16674  dmdprd  16832  dprdcntz2  16888  dprd2d2  16895  isnzr2  17710  mpfind  18004  gsummoncoe1  18145  pf1ind  18190  chrdvds  18360  chrcong  18361  znleval  18388  isphld  18484  smadiadetr  18972  mp2pm2mplem4  19105  isclo  19382  ist1-2  19642  isnrm2  19653  bwth  19704  bwthOLD  19705  nconsubb  19718  subislly  19776  ptclsg  19879  qtopcld  19977  kqcldsat  19997  divstgplem  20382  tsmssubm  20407  ustuqtop  20512  utop2nei  20516  blval2  20841  caucfil  21485  ioorinv  21748  mbfss  21816  iblss2  21975  dvivthlem1  22172  lhop1  22178  deg1leb  22258  reeff1o  22604  sincosq3sgn  22654  sincosq4sgn  22655  dcubic  22933  efrlim  23055  fsumharmonic  23097  isppw  23144  issqf  23166  fsumdvdsmul  23227  ppiub  23235  lgsdinn0  23371  tglngne  23693  tgelrnln  23752  tghilbert1_1  23759  axlowdimlem14  23962  uhgraop  24008  eupath2lem2  24682  h2hlm  25601  isch2  25845  ch0pss  26067  nmcfnlbi  26675  jplem1  26891  hatomistici  26985  mdsymlem5  27030  cdjreui  27055  reuxfr4d  27093  dfimafnf  27174  funcnvmpt  27210  fpwrelmap  27256  nn0min  27307  isarchi  27416  ordtconlem1  27570  esumfsup  27744  esumpcvgval  27752  measvuni  27853  aean  27884  eulerpartlemgh  27985  ballotlemsima  28122  sgn3da  28148  subfacp1lem2a  28292  subfacp1lem6  28297  ghomf1olem  28537  rtrclreclem.trans  28572  dfres3  28793  eldm3  28796  onsuct0  29511  ptrest  29653  sdclem2  29866  fdc  29869  fdc1  29870  istotbnd3  29898  sstotbnd  29902  prdstotbnd  29921  rrncmslem  29959  diophin  30338  diophun  30339  diophrex  30341  3rexfrabdioph  30362  6rexfrabdioph  30364  7rexfrabdioph  30365  zindbi  30514  isprm7  30823  hashnzfzclim  30855  fveqsb  30968  cncfiooicclem1  31260  stoweidlem35  31363  tz6.12-afv  31753  ndmaovg  31764  isfusgracl  31921  isfusgraclALT  31923  usgfis  31941  usgfisALT  31945  bnj1468  33001  lub0N  34004  glb0N  34008  cdlemefrs29bpre0  35210  dvhb1dimN  35800  dvhopellsm  35932  dibord  35974  dochnel2  36207  mapdvalc  36444  mapdval4N  36447
  Copyright terms: Public domain W3C validator