Theorem mpancom 689

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	⊢ (𝜓 → 𝜑)
mpancom.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpancom	⊢ (𝜓 → 𝜒)

Proof of Theorem mpancom

Step	Hyp	Ref	Expression
1		mpancom.1	. 2 ⊢ (𝜓 → 𝜑)
2		id 22	. 2 ⊢ (𝜓 → 𝜓)
3		mpancom.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpan  691  spesbc  3834  csbie2df  4397  xpiindi  5792  fununfun  6548  dffv2  6937  fliftcnv  7267  riotaprop  7352  elovmpt3rab1  7628  3xpexg  7707  orduniorsuc  7782  unielxp  7981  dmtpos  8190  tpossym  8210  oesuclem  8462  ercnv  8667  cnvct  8983  sucxpdom  9173  enp1i  9191  pwfilem  9230  3xpfi  9233  rankr1id  9786  cardnn  9887  alephnbtwn2  9994  alephsucdom  10001  cdainflem  10110  isfin4p1  10237  axcclem  10379  dmct  10446  mptct  10460  infxpidm  10484  fpwwe2lem8  10561  gchpwdom  10593  elwina  10609  elina  10610  rankcf  10700  ltexprlem4  10962  lem1  11996  ltdivp1i  12080  nn0le2x  12467  rpnnen1lem5  12906  eluzfz1  13459  fzpred  13500  uznfz  13538  fz0fzdiffz0  13565  fzctr  13568  flid  13740  modid0  13829  2txmodxeq0  13866  faclbnd3  14227  faclbnd4lem4  14231  bcn1  14248  hashfac  14393  repswsymballbi  14715  wrdlen2i  14877  dfrtrclrec2  14993  rtrclreclem3  14995  rtrclreclem4  14996  relexpindlem  14998  sqrtsq  15204  absrdbnd  15277  sqreulem  15295  sqreu  15296  bpoly2  15992  bpoly3  15993  gcd0id  16458  lcmgcdlem  16545  lcmftp  16575  dvdsnprmd  16629  2mulprm  16632  pcprod  16835  fldivp1  16837  invsym2  17699  pleval2i  18269  smndlsmidm  19597  gsumle  20086  subrgsubm  20530  resrhm2b  20547  cncrngOLD  21356  pzriprnglem11  21458  znchr  21529  psrbagfsupp  21887  mattposvs  22411  smadiadetglem2  22628  tg1  22920  cldval  22979  cldss  22985  cldopn  22987  1stcrestlem  23408  refbas  23466  refssex  23467  regr1  23706  kqreg  23707  kqnrm  23708  ufilen  23886  efmndtmd  24057  symgtgp  24062  psmetdmdm  24261  icoopnst  24904  cnheiborlem  24921  cfilfcls  25242  eflogeq  26579  logdivlt  26598  logdifbnd  26972  harmonicbnd4  26989  basellem5  27063  bposlem7  27269  zabsle1  27275  addsqn2reu  27420  chto1ub  27455  chpo1ub  27459  vmadivsum  27461  dchrmusum2  27473  dchrvmasum2if  27476  dchrvmasumlema  27479  dchrvmasumiflem2  27481  dchrisum0re  27492  dchrvmasumlem  27502  rplogsum  27506  mulogsumlem  27510  logdivsum  27512  selberg2lem  27529  pntrmax  27543  pntlem3  27588  pntleml  27590  pnt2  27592  noextendlt  27649  usgredg2vlem2  29311  vtxdgelxnn0  29558  wlkonprop  29742  wksonproplem  29788  wwlknbp  29927  wspthnp  29935  wlklnwwlkln1  29953  clwwlkf  30134  erclwwlknsym  30157  erclwwlkntr  30158  eupth0  30301  numclwwlk1lem2fo  30445  numclwlk2lem2f  30464  numclwwlk5lem  30474  hilablo  31247  hhssabloilem  31348  mayete3i  31815  homullid  31887  adjeu  31976  lnopeqi  32095  cnlnadjlem7  32160  adjbdlnb  32171  nmopcoadji  32188  bracnlnval  32201  mptctf  32805  xraddge02  32847  xrge0npcan  33112  gsumvsca1  33319  gsumvsca2  33320  baselsiga  34292  sigasspw  34293  ddeval1  34411  ddeval0  34412  braew  34419  derangen2  35387  subfaclim  35401  snmlff  35542  elfzm12  35888  fnetr  36564  wl-sbal1  37815  poimirlem13  37881  poimirlem14  37882  poimirlem31  37899  poimirlem32  37900  ismblfin  37909  itg2addnclem2  37920  areacirclem2  37957  areacirc  37961  ismgmOLD  38098  ismndo2  38122  rngomndo  38183  ecxrn2  38656  dmqseq  38972  prter3  39255  atbase  39662  llnbase  39882  lplnbase  39907  lvolbase  39951  lhpbase  40371  rernegcl  42738  renegadd  42739  reneg0addlid  42741  sn-0ne2  42773  3cubes  43044  mzpsubmpt  43097  mzpnegmpt  43098  eliunov2  44032  iunrelexp0  44055  enmappwid  44353  uunT1  45132  nnfoctb  45405  rn1st  45628  afveu  47510  afv2eu  47595  afv20fv0  47620  fzopredsuc  47680  fargshiftfva  47800  lindsrng01  48825  cic1st2nd  49403  cicpropdlem  49405  zeroo2  49590