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  3828  csbie2df  4390  xpiindi  5774  fununfun  6529  dffv2  6917  fliftcnv  7245  riotaprop  7330  elovmpt3rab1  7606  3xpexg  7685  orduniorsuc  7760  unielxp  7959  dmtpos  8168  tpossym  8188  oesuclem  8440  ercnv  8643  cnvct  8956  sucxpdom  9145  enp1i  9163  pwfilem  9202  3xpfi  9205  rankr1id  9755  cardnn  9856  alephnbtwn2  9963  alephsucdom  9970  cdainflem  10079  isfin4p1  10206  axcclem  10348  dmct  10415  mptct  10429  infxpidm  10453  fpwwe2lem8  10529  gchpwdom  10561  elwina  10577  elina  10578  rankcf  10668  ltexprlem4  10930  lem1  11964  ltdivp1i  12048  nn0le2x  12435  rpnnen1lem5  12879  eluzfz1  13431  fzpred  13472  uznfz  13510  fz0fzdiffz0  13537  fzctr  13540  flid  13712  modid0  13801  2txmodxeq0  13838  faclbnd3  14199  faclbnd4lem4  14203  bcn1  14220  hashfac  14365  repswsymballbi  14687  wrdlen2i  14849  dfrtrclrec2  14965  rtrclreclem3  14967  rtrclreclem4  14968  relexpindlem  14970  sqrtsq  15176  absrdbnd  15249  sqreulem  15267  sqreu  15268  bpoly2  15964  bpoly3  15965  gcd0id  16430  lcmgcdlem  16517  lcmftp  16547  dvdsnprmd  16601  2mulprm  16604  pcprod  16807  fldivp1  16809  invsym2  17670  pleval2i  18240  smndlsmidm  19568  gsumle  20057  subrgsubm  20500  resrhm2b  20517  cncrngOLD  21326  pzriprnglem11  21428  znchr  21499  psrbagfsupp  21856  mattposvs  22370  smadiadetglem2  22587  tg1  22879  cldval  22938  cldss  22944  cldopn  22946  1stcrestlem  23367  refbas  23425  refssex  23426  regr1  23665  kqreg  23666  kqnrm  23667  ufilen  23845  efmndtmd  24016  symgtgp  24021  psmetdmdm  24220  icoopnst  24863  cnheiborlem  24880  cfilfcls  25201  eflogeq  26538  logdivlt  26557  logdifbnd  26931  harmonicbnd4  26948  basellem5  27022  bposlem7  27228  zabsle1  27234  addsqn2reu  27379  chto1ub  27414  chpo1ub  27418  vmadivsum  27420  dchrmusum2  27432  dchrvmasum2if  27435  dchrvmasumlema  27438  dchrvmasumiflem2  27440  dchrisum0re  27451  dchrvmasumlem  27461  rplogsum  27465  mulogsumlem  27469  logdivsum  27471  selberg2lem  27488  pntrmax  27502  pntlem3  27547  pntleml  27549  pnt2  27551  noextendlt  27608  usgredg2vlem2  29204  vtxdgelxnn0  29451  wlkonprop  29635  wksonproplem  29681  wwlknbp  29820  wspthnp  29828  wlklnwwlkln1  29846  clwwlkf  30027  erclwwlknsym  30050  erclwwlkntr  30051  eupth0  30194  numclwwlk1lem2fo  30338  numclwlk2lem2f  30357  numclwwlk5lem  30367  hilablo  31140  hhssabloilem  31241  mayete3i  31708  homullid  31780  adjeu  31869  lnopeqi  31988  cnlnadjlem7  32053  adjbdlnb  32064  nmopcoadji  32081  bracnlnval  32094  mptctf  32699  xraddge02  32740  xrge0npcan  33001  gsumvsca1  33195  gsumvsca2  33196  baselsiga  34128  sigasspw  34129  ddeval1  34247  ddeval0  34248  braew  34255  derangen2  35218  subfaclim  35232  snmlff  35373  elfzm12  35719  fnetr  36395  wl-sbal1  37607  poimirlem13  37672  poimirlem14  37673  poimirlem31  37690  poimirlem32  37691  ismblfin  37700  itg2addnclem2  37711  areacirclem2  37748  areacirc  37752  ismgmOLD  37889  ismndo2  37913  rngomndo  37974  ecxrn2  38431  dmqseq  38736  prter3  38980  atbase  39387  llnbase  39607  lplnbase  39632  lvolbase  39676  lhpbase  40096  rernegcl  42463  renegadd  42464  reneg0addlid  42466  sn-0ne2  42498  3cubes  42782  mzpsubmpt  42835  mzpnegmpt  42836  eliunov2  43771  iunrelexp0  43794  enmappwid  44092  uunT1  44871  nnfoctb  45144  rn1st  45369  afveu  47252  afv2eu  47337  afv20fv0  47362  fzopredsuc  47422  fargshiftfva  47542  lindsrng01  48568  cic1st2nd  49147  cicpropdlem  49149  zeroo2  49334