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  1941  19.19  1943  sbcom2  2173  sbal2  2189  cbvabOLD  2583  necon1bbid  2691  necon4abidOLD  2693  elabgt  3227  sbceq1a  3322  sbcralt  3392  sbccsbgOLD  3832  sbccsb2  3833  sbccsb2gOLD  3834  disjxun  4431  xp11  5428  ressn  5529  fnssresb  5679  dmfco  5928  dffo4  6028  f1ompt  6034  funressn  6065  fnsuppeq0OLD  6113  elunirnALT  6145  fliftf  6194  resoprab2  6380  elrnmpt2res  6397  ralrnmpt2  6398  iunpw  6595  ordunisuc2  6660  tfis  6670  tfinds  6675  dfom2  6683  fun11iun  6741  opiota  6840  1stconst  6869  2ndconst  6870  fnsuppeq0  6926  iinon  7009  dfsmo2  7016  oeeui  7249  omabs  7294  brecop  7402  ixpsnf1o  7507  boxcutc  7510  ac6sfi  7762  wemapwe  8137  wemapweOLD  8138  sdom2en01  8680  ac6num  8857  zorn2lem7  8880  ttukeylem6  8892  alephval2  8945  fpwwe2  9019  fpwwe  9022  nqereu  9305  suplem2pr  9429  map2psrpr  9485  supsrlem  9486  fimaxre3  10493  infm3  10503  crne0  10530  nn1suc  10558  uzindOLD  10958  xmulneg1  11465  supxrbnd1  11517  supxrbnd2  11518  iccneg  11645  wrdmap  12546  wrdind  12676  cnpart  13047  sqrt00  13071  lo1resb  13361  o1resb  13363  absefib  13805  efieq1re  13806  sadadd2lem2  13972  saddisjlem  13986  prmind2  14100  mreacs  14927  issubc  15076  isfunc  15102  pospo  15472  mrcmndind  15866  eqgval  16119  resscntz  16238  frgpuplem  16659  qusabl  16740  dmdprd  16898  dprdcntz2  16954  dprd2d2  16961  isnzr2  17779  mpfind  18073  gsummoncoe1  18214  pf1ind  18259  chrdvds  18432  chrcong  18433  znleval  18460  isphld  18556  smadiadetr  19044  mp2pm2mplem4  19177  isclo  19454  ist1-2  19714  isnrm2  19725  bwth  19776  bwthOLD  19777  nconsubb  19790  subislly  19848  ptclsg  19982  qtopcld  20080  kqcldsat  20100  qustgplem  20485  tsmssubm  20510  ustuqtop  20615  utop2nei  20619  blval2  20944  caucfil  21588  ioorinv  21851  mbfss  21919  iblss2  22078  dvivthlem1  22275  lhop1  22281  deg1leb  22361  reeff1o  22707  sincosq3sgn  22758  sincosq4sgn  22759  dcubic  23042  efrlim  23164  fsumharmonic  23206  isppw  23253  issqf  23275  fsumdvdsmul  23336  ppiub  23344  lgsdinn0  23480  tglngne  23802  tgelrnln  23875  axlowdimlem14  24123  uhgraop  24169  eupath2lem2  24843  h2hlm  25762  isch2  26006  ch0pss  26228  nmcfnlbi  26836  jplem1  27052  hatomistici  27146  mdsymlem5  27191  cdjreui  27216  reuxfr4d  27254  dfimafnf  27338  funcnvmpt  27375  fpwrelmap  27421  nn0min  27477  isarchi  27592  ordtconlem1  27772  esumfsup  27942  esumpcvgval  27950  measvuni  28051  aean  28082  eulerpartlemgh  28183  ballotlemsima  28320  sgn3da  28346  subfacp1lem2a  28490  subfacp1lem6  28495  ghomf1olem  28900  rtrclreclem.trans  28935  dfres3  29156  eldm3  29159  onsuct0  29874  ptrest  30016  sdclem2  30203  fdc  30206  fdc1  30207  istotbnd3  30235  sstotbnd  30239  prdstotbnd  30258  rrncmslem  30296  diophin  30674  diophun  30675  diophrex  30677  3rexfrabdioph  30698  6rexfrabdioph  30700  7rexfrabdioph  30701  zindbi  30850  isprm7  31161  hashnzfzclim  31196  fveqsb  31309  cncfiooicclem1  31599  stoweidlem35  31702  tz6.12-afv  32092  ndmaovg  32103  isfusgracl  32260  isfusgraclALT  32262  usgfis  32280  usgfisALT  32284  bnj1468  33611  lub0N  34616  glb0N  34620  cdlemefrs29bpre0  35824  dvhb1dimN  36414  dvhopellsm  36546  dibord  36588  dochnel2  36821  mapdvalc  37058  mapdval4N  37061
  Copyright terms: Public domain W3C validator