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

Theorem mpancom 652
Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpancom.1  |-  ( ps 
->  ph )
mpancom.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mpancom  |-  ( ps 
->  ch )

Proof of Theorem mpancom
StepHypRef Expression
1 mpancom.1 . 2  |-  ( ps 
->  ph )
2 id 21 . 2  |-  ( ps 
->  ps )
3 mpancom.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 644 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  mpan  653  spesbc  3244  orduniorsuc  4813  xpiindi  5013  dffv2  5799  fliftcnv  6036  unielxp  6388  dmtpos  6494  tpossym  6514  riotaprop  6576  oesuclem  6772  ercnv  6929  undom  7199  sucxpdom  7321  pwfilem  7404  rankr1id  7791  cardnn  7855  alephnbtwn2  7958  alephsucdom  7965  cdainflem  8076  isfin4-3  8200  axcclem  8342  infxpidm  8442  fpwwe2lem9  8518  gchpwdom  8550  elwina  8566  elina  8567  rankcf  8657  ltexprlem4  8921  lem1  9856  ltdivp1i  9942  rpnnen1lem5  10609  eluzfz1  11069  fzctr  11122  uznfz  11135  flid  11221  faclbnd3  11588  faclbnd4lem4  11592  bcn1  11609  hashfac  11712  sqrsq  12080  absrdbnd  12150  sqreulem  12168  sqreu  12169  gcd0id  13028  pcprod  13269  fldivp1  13271  invsym2  13993  pleval2i  14426  subrgsubm  15886  cncrng  16727  znchr  16848  tg1  17034  cldval  17092  cldss  17098  cldopn  17100  1stcrestlem  17520  regr1  17787  kqreg  17788  kqnrm  17789  ufilen  17967  symgtgp  18136  elrnust  18259  psmetdmdm  18341  metuvalOLD  18584  metuval  18585  icoopnst  18969  cnheiborlem  18984  cfilfcls  19232  eflogeq  20501  logdivlt  20521  logdifbnd  20837  harmonicbnd4  20854  basellem5  20872  bposlem7  21079  chto1ub  21175  chpo1ub  21179  vmadivsum  21181  dchrmusum2  21193  dchrvmasum2if  21196  dchrvmasumlema  21199  dchrvmasumiflem2  21201  dchrisum0re  21212  dchrvmasumlem  21222  rplogsum  21226  mulogsumlem  21230  logdivsum  21232  selberg2lem  21249  pntrmax  21263  pntlem3  21308  pntleml  21310  pnt2  21312  usgraidx2vlem2  21416  nbcusgra  21477  uvtxnbgravtx  21509  cusgrauvtxb  21510  wlkonprop  21537  wlkbprop  21539  trlonprop  21547  pthonprop  21582  spthonprp  21590  cyclispthon  21625  fargshiftfva  21631  constr3lem4  21639  constr3trllem2  21643  4cycl4dv  21659  eupatrl  21695  issubgoi  21903  ismgm  21913  ismndo2  21938  ablomul  21948  rngomndo  22014  vcoprnelem  22062  hilablo  22667  mayete3i  23235  mayete3iOLD  23236  homulid2  23308  adjeu  23397  lnopeqi  23516  cnlnadjlem7  23581  adjbdlnb  23592  nmopcoadji  23609  bracnlnval  23622  elunirn2  24068  dmct  24111  cnvct  24112  mptct  24114  mptctf  24117  xraddge02  24128  xrge0npcan  24221  metidval  24290  pstmval  24295  baselsiga  24503  sigasspw  24504  braew  24598  derangen2  24865  subfaclim  24879  snmlff  25021  elfzm12  25117  relexp0  25134  relexpsucr  25135  relexp1  25136  relexpcnv  25138  relexpadd  25143  relexpindlem  25144  dfrtrclrec2  25148  rtrclreclem.trans  25151  rtrclreclem.min  25152  bpoly2  26108  ismblfin  26259  itg2addnclem2  26271  areacirclem2  26307  areacirc  26311  refbas  26374  refssex  26375  fnetr  26380  prter3  26745  mzpsubmpt  26814  mzpnegmpt  26815  afveu  28007  3xpexg  28068  3xpfi  28110  fz0fzdiffz0  28142  modid0  28182  2txmodxeq0  28185  hash2prv  28193  hash2sspr  28194  wrdlenge2n0  28208  swrdtrcfv0  28229  swrdtrcfvl  28299  cshweqdif2s  28305  usgra2pthspth  28343  usgra2adedgspthlem1  28351  usgra2adedgwlk  28354  wlklniswwlkn1  28381  2wlkonot  28397  2spthonot  28398  2spotfi  28424  frgra1v  28462  frgrancvvdeqlem3  28495  2spotmdisj  28531  uunT1  28966  atbase  30161  llnbase  30380  lplnbase  30405  lvolbase  30449  lhpbase  30869
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 179  df-an 362
  Copyright terms: Public domain W3C validator