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  357  19.16  1962  19.19  1964  sbcom2  2191  sbal2  2207  cbvabOLD  2596  necon1bbid  2704  necon4abidOLD  2706  elabgt  3240  sbceq1a  3335  sbcralt  3397  sbccsb2  3844  disjxun  4437  xp11  5427  ressn  5526  fnssresb  5675  dmfco  5922  dffo4  6023  f1ompt  6029  funressn  6060  elunirnALT  6139  fliftf  6188  resoprab2  6372  elrnmpt2res  6389  ralrnmpt2  6390  iunpw  6587  ordunisuc2  6652  tfis  6662  tfinds  6667  dfom2  6675  fun11iun  6733  opiota  6832  1stconst  6861  2ndconst  6862  fnsuppeq0  6920  iinon  7003  dfsmo2  7010  oeeui  7243  omabs  7288  brecop  7396  ixpsnf1o  7502  boxcutc  7505  ac6sfi  7756  wemapwe  8130  wemapweOLD  8131  sdom2en01  8673  ac6num  8850  zorn2lem7  8873  ttukeylem6  8885  alephval2  8938  fpwwe2  9010  fpwwe  9013  nqereu  9296  suplem2pr  9420  map2psrpr  9476  supsrlem  9477  fimaxre3  10487  infm3  10497  crne0  10524  nn1suc  10552  uzindOLD  10953  xmulneg1  11464  supxrbnd1  11516  supxrbnd2  11517  iccneg  11644  wrdmap  12560  wrdind  12693  rtrclreclem3  12975  cnpart  13155  sqrt00  13179  lo1resb  13469  o1resb  13471  absefib  14015  efieq1re  14016  sadadd2lem2  14184  saddisjlem  14198  prmind2  14312  mreacs  15147  issubc  15323  isfunc  15352  pospo  15802  mrcmndind  16196  eqgval  16449  resscntz  16568  frgpuplem  16989  qusabl  17070  dmdprd  17224  dprdcntz2  17281  dprd2d2  17288  isnzr2  18106  mpfind  18400  gsummoncoe1  18541  pf1ind  18586  chrdvds  18740  chrcong  18741  znleval  18766  isphld  18862  smadiadetr  19344  mp2pm2mplem4  19477  isclo  19755  ist1-2  20015  isnrm2  20026  bwth  20077  nconsubb  20090  subislly  20148  ptclsg  20282  qtopcld  20380  kqcldsat  20400  qustgplem  20785  tsmssubm  20810  ustuqtop  20915  utop2nei  20919  blval2  21244  caucfil  21888  ioorinv  22151  mbfss  22219  iblss2  22378  dvivthlem1  22575  lhop1  22581  deg1leb  22661  reeff1o  23008  sincosq3sgn  23059  sincosq4sgn  23060  dcubic  23374  efrlim  23497  fsumharmonic  23539  isppw  23586  issqf  23608  fsumdvdsmul  23669  ppiub  23677  lgsdinn0  23813  tglngne  24138  tgelrnln  24211  axlowdimlem14  24460  uhgraop  24506  eupath2lem2  25180  h2hlm  26095  isch2  26339  ch0pss  26561  nmcfnlbi  27169  jplem1  27385  hatomistici  27479  mdsymlem5  27524  cdjreui  27549  reuxfr4d  27587  dfimafnf  27694  funcnvmpt  27737  fpwrelmap  27787  nn0min  27845  isarchi  27960  ordtconlem1  28141  esumfsup  28299  esumpcvgval  28307  measvuni  28422  aean  28453  eulerpartlemgh  28581  ballotlemsima  28718  sgn3da  28744  subfacp1lem2a  28888  subfacp1lem6  28893  ghomf1olem  29298  dfres3  29429  eldm3  29432  onsuct0  30134  ptrest  30288  sdclem2  30475  fdc  30478  fdc1  30479  istotbnd3  30507  sstotbnd  30511  prdstotbnd  30530  rrncmslem  30568  diophin  30945  diophun  30946  diophrex  30948  3rexfrabdioph  30970  6rexfrabdioph  30972  7rexfrabdioph  30973  zindbi  31121  isprm7  31433  hashnzfzclim  31468  fveqsb  31603  cncfiooicclem1  31935  stoweidlem35  32056  tz6.12-afv  32497  ndmaovg  32508  isfusgracl  32798  isfusgraclALT  32800  usgfis  32818  usgfisALT  32822  aacllem  33604  bnj1468  34305  lub0N  35311  glb0N  35315  cdlemefrs29bpre0  36519  dvhb1dimN  37109  dvhopellsm  37241  dibord  37283  dochnel2  37516  mapdvalc  37753  mapdval4N  37756  relexpnul  38199
  Copyright terms: Public domain W3C validator