Theorem mpancom 688

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 584	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  690  spesbc  3864  csbie2df  4425  xpiindi  5828  fununfun  6595  dffv2  6985  elunirn2OLD  7256  fliftcnv  7314  riotaprop  7398  elovmpt3rab1  7676  3xpexg  7755  orduniorsuc  7833  unielxp  8035  dmtpos  8246  tpossym  8266  wfrlem5OLD  8336  oesuclem  8546  ercnv  8749  cnvct  9057  undomOLD  9083  sucxpdom  9274  enp1i  9296  pwfilem  9339  3xpfi  9343  rankr1id  9885  cardnn  9986  alephnbtwn2  10095  alephsucdom  10102  cdainflem  10211  isfin4p1  10338  axcclem  10480  dmct  10547  mptct  10561  infxpidm  10585  fpwwe2lem8  10661  gchpwdom  10693  elwina  10709  elina  10710  rankcf  10800  ltexprlem4  11062  lem1  12093  ltdivp1i  12177  nn0le2x  12564  rpnnen1lem5  13006  eluzfz1  13554  fzpred  13595  uznfz  13633  fz0fzdiffz0  13660  fzctr  13663  flid  13831  modid0  13920  2txmodxeq0  13955  faclbnd3  14314  faclbnd4lem4  14318  bcn1  14335  hashfac  14480  repswsymballbi  14801  wrdlen2i  14964  dfrtrclrec2  15080  rtrclreclem3  15082  rtrclreclem4  15083  relexpindlem  15085  sqrtsq  15291  absrdbnd  15363  sqreulem  15381  sqreu  15382  bpoly2  16076  bpoly3  16077  gcd0id  16539  lcmgcdlem  16626  lcmftp  16656  dvdsnprmd  16710  2mulprm  16713  pcprod  16916  fldivp1  16918  invsym2  17783  pleval2i  18355  smndlsmidm  19647  subrgsubm  20558  resrhm2b  20575  cncrngOLD  21369  pzriprnglem11  21469  znchr  21548  psrbagfsupp  21906  mattposvs  22428  smadiadetglem2  22645  tg1  22937  cldval  22996  cldss  23002  cldopn  23004  1stcrestlem  23425  refbas  23483  refssex  23484  regr1  23723  kqreg  23724  kqnrm  23725  ufilen  23903  efmndtmd  24074  symgtgp  24079  psmetdmdm  24279  icoopnst  24924  cnheiborlem  24941  cfilfcls  25263  eflogeq  26599  logdivlt  26618  logdifbnd  26992  harmonicbnd4  27009  basellem5  27083  bposlem7  27289  zabsle1  27295  addsqn2reu  27440  chto1ub  27475  chpo1ub  27479  vmadivsum  27481  dchrmusum2  27493  dchrvmasum2if  27496  dchrvmasumlema  27499  dchrvmasumiflem2  27501  dchrisum0re  27512  dchrvmasumlem  27522  rplogsum  27526  mulogsumlem  27530  logdivsum  27532  selberg2lem  27549  pntrmax  27563  pntlem3  27608  pntleml  27610  pnt2  27612  noextendlt  27669  usgredg2vlem2  29190  vtxdgelxnn0  29437  wlkonprop  29623  wksonproplem  29669  wksonproplemOLD  29670  wwlknbp  29809  wspthnp  29817  wlklnwwlkln1  29835  clwwlkf  30013  erclwwlknsym  30036  erclwwlkntr  30037  eupth0  30180  numclwwlk1lem2fo  30324  numclwlk2lem2f  30343  numclwwlk5lem  30353  hilablo  31126  hhssabloilem  31227  mayete3i  31694  homullid  31766  adjeu  31855  lnopeqi  31974  cnlnadjlem7  32039  adjbdlnb  32050  nmopcoadji  32067  bracnlnval  32080  mptctf  32676  xraddge02  32707  xrge0npcan  32971  gsumle  33047  gsumvsca1  33178  gsumvsca2  33179  baselsiga  34057  sigasspw  34058  ddeval1  34176  ddeval0  34177  braew  34184  derangen2  35120  subfaclim  35134  snmlff  35275  elfzm12  35621  fnetr  36293  wl-sbal1  37505  poimirlem13  37581  poimirlem14  37582  poimirlem31  37599  poimirlem32  37600  ismblfin  37609  itg2addnclem2  37620  areacirclem2  37657  areacirc  37661  ismgmOLD  37798  ismndo2  37822  rngomndo  37883  cnvepimaex  38278  dmqseq  38582  prter3  38824  atbase  39231  llnbase  39452  lplnbase  39477  lvolbase  39521  lhpbase  39941  rernegcl  42346  renegadd  42347  reneg0addlid  42349  sn-0ne2  42381  3cubes  42646  mzpsubmpt  42699  mzpnegmpt  42700  eliunov2  43637  iunrelexp0  43660  enmappwid  43958  uunT1  44745  nnfoctb  44998  rn1st  45225  afveu  47111  afv2eu  47196  afv20fv0  47221  fzopredsuc  47281  fargshiftfva  47376  lindsrng01  48331