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

Theorem mpancom 651
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 20 . 2  |-  ( ps 
->  ps )
3 mpancom.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 643 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpan  652  spesbc  3210  orduniorsuc  4777  xpiindi  4977  dffv2  5763  fliftcnv  6000  unielxp  6352  dmtpos  6458  tpossym  6478  riotaprop  6540  oesuclem  6736  ercnv  6893  undom  7163  sucxpdom  7285  pwfilem  7367  rankr1id  7752  cardnn  7814  alephnbtwn2  7917  alephsucdom  7924  cdainflem  8035  isfin4-3  8159  axcclem  8301  infxpidm  8401  fpwwe2lem9  8477  gchpwdom  8513  elwina  8525  elina  8526  rankcf  8616  ltexprlem4  8880  lem1  9815  ltdivp1i  9901  rpnnen1lem5  10568  eluzfz1  11028  fzctr  11080  uznfz  11093  flid  11179  faclbnd3  11546  faclbnd4lem4  11550  bcn1  11567  hashfac  11670  sqrsq  12038  absrdbnd  12108  sqreulem  12126  sqreu  12127  gcd0id  12986  pcprod  13227  fldivp1  13229  invsym2  13951  pleval2i  14384  subrgsubm  15844  cncrng  16685  znchr  16806  tg1  16992  cldval  17050  cldss  17056  cldopn  17058  1stcrestlem  17476  regr1  17743  kqreg  17744  kqnrm  17745  ufilen  17923  symgtgp  18092  elrnust  18215  psmetdmdm  18297  metuvalOLD  18540  metuval  18541  icoopnst  18925  cnheiborlem  18940  cfilfcls  19188  eflogeq  20457  logdivlt  20477  logdifbnd  20793  harmonicbnd4  20810  basellem5  20828  bposlem7  21035  chto1ub  21131  chpo1ub  21135  vmadivsum  21137  dchrmusum2  21149  dchrvmasum2if  21152  dchrvmasumlema  21155  dchrvmasumiflem2  21157  dchrisum0re  21168  dchrvmasumlem  21178  rplogsum  21182  mulogsumlem  21186  logdivsum  21188  selberg2lem  21205  pntrmax  21219  pntlem3  21264  pntleml  21266  pnt2  21268  usgraidx2vlem2  21372  nbcusgra  21433  uvtxnbgravtx  21465  cusgrauvtxb  21466  wlkonprop  21493  wlkbprop  21495  trlonprop  21503  pthonprop  21538  spthonprp  21546  cyclispthon  21581  fargshiftfva  21587  constr3lem4  21595  constr3trllem2  21599  4cycl4dv  21615  eupatrl  21651  issubgoi  21859  ismgm  21869  ismndo2  21894  ablomul  21904  rngomndo  21970  vcoprnelem  22018  hilablo  22623  mayete3i  23191  mayete3iOLD  23192  homulid2  23264  adjeu  23353  lnopeqi  23472  cnlnadjlem7  23537  adjbdlnb  23548  nmopcoadji  23565  bracnlnval  23578  elunirn2  24024  dmct  24067  cnvct  24068  mptct  24070  mptctf  24073  xraddge02  24084  xrge0npcan  24177  metidval  24246  pstmval  24251  baselsiga  24459  sigasspw  24460  braew  24554  derangen2  24821  subfaclim  24835  snmlff  24977  elfzm12  25073  relexp0  25090  relexpsucr  25091  relexp1  25092  relexpcnv  25094  relexpadd  25099  relexpindlem  25100  dfrtrclrec2  25104  rtrclreclem.trans  25107  rtrclreclem.min  25108  fallfacfac  25310  bpoly2  26015  ismblfin  26154  itg2addnclem2  26164  areacirclem4  26191  areacirc  26195  refbas  26258  refssex  26259  fnetr  26264  prter3  26629  mzpsubmpt  26698  mzpnegmpt  26699  afveu  27892  3xpexg  27950  3xpfi  27975  usgra2pthspth  28043  usgra2adedgspthlem1  28051  usgra2adedgwlk  28054  2wlkonot  28070  2spthonot  28071  2spotfi  28097  frgra1v  28110  frgrancvvdeqlem3  28143  2spotmdisj  28179  uunT1  28610  atbase  29784  llnbase  30003  lplnbase  30028  lvolbase  30072  lhpbase  30492
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator