Theorem mpancom 701

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 23	. 2 ⊢ (𝜓 → 𝜓)
3		mpancom.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜓 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpan  703  spesbc  3828  csbie2df  4400  xpiindi  5811  fununfun  6588  dffv2  6980  fliftcnv  7319  riotaprop  7404  elovmpt3rab1  7681  3xpexg  7766  orduniorsuc  7841  unielxp  8039  dmtpos  8258  tpossym  8278  oesuclem  8536  ercnv  8742  cnvct  9065  sucxpdom  9255  enp1i  9273  pwfilem  9312  3xpfi  9315  rankr1id  9881  cardnn  10047  alephnbtwn2  10154  alephsucdom  10161  cdainflem  10269  isfin4p1  10396  axcclem  10538  dmct  10605  dmctOLD  10606  mptct  10625  infxpidm  10649  fpwwe2lem8  10726  gchpwdom  10758  elwina  10774  elina  10775  rankcf  10865  ltexprlem4  11127  lem1  12163  ltdivp1i  12246  nn0le2x  12663  rpnnen1lem5  13112  eluzfz1  13667  fzpred  13709  uznfz  13747  fz0fzdiffz0  13774  flid  13951  modid0  14040  2txmodxeq0  14077  faclbnd3  14439  faclbnd4lem4  14443  bcn1  14460  hashfac  14606  repswsymballbi  14935  wrdlen2i  15098  dfrtrclrec2  15216  rtrclreclem3  15218  rtrclreclem4  15219  relexpindlem  15221  sqrtsq  15441  absrdbnd  15514  sqreulem  15532  sqreu  15533  bpoly2  16228  bpoly3  16229  gcd0id  16696  lcmgcdlem  16786  lcmftp  16816  dvdsnprmd  16870  2mulprm  16873  pcprod  17078  fldivp1  17080  invsym2  17943  pleval2i  18513  smndlsmidm  19875  gsumle  20364  subrgsubm  20842  resrhm2b  20859  pzriprnglem11  21802  znchr  21873  psrbagfsupp  22232  mattposvs  22775  smadiadetglem2  22992  tg1  23287  cldval  23346  cldss  23352  cldopn  23354  1stcrestlem  23775  refbas  23834  refssex  23835  regr1  24074  kqreg  24075  kqnrm  24076  ufilen  24254  efmndtmd  24425  symgtgp  24430  psmetdmdm  24629  icoopnst  25265  cnheiborlem  25280  cfilfcls  25600  eflogeq  26935  logdivlt  26954  logdifbnd  27326  harmonicbnd4  27343  basellem5  27417  bposlem7  27622  zabsle1  27628  addsqn2reu  27773  chto1ub  27808  chpo1ub  27812  vmadivsum  27814  dchrmusum2  27826  dchrvmasum2if  27829  dchrvmasumlema  27832  dchrvmasumiflem2  27834  dchrisum0re  27845  dchrvmasumlem  27855  rplogsum  27859  mulogsumlem  27863  logdivsum  27865  selberg2lem  27882  pntrmax  27896  pntlem3  27941  pntleml  27943  pnt2  27945  noextendlt  28031  usgredg2vlem2  29812  vtxdgelxnn0  30058  wlkonprop  30242  wksonproplem  30292  wwlknbp  30436  wspthnp  30444  wlklnwwlkln1  30462  clwwlkf  30643  erclwwlknsym  30666  erclwwlkntr  30667  eupth0  30820  numclwwlk1lem2fo  30964  numclwlk2lem2f  30983  numclwwlk5lem  30993  hilablo  31767  hhssabloilem  31868  mayete3i  32335  homullid  32407  adjeu  32496  lnopeqi  32615  cnlnadjlem7  32680  adjbdlnb  32691  nmopcoadji  32708  bracnlnval  32721  mptctf  33355  xraddge02  33395  xrge0npcan  33627  gsumvsca1  33833  gsumvsca2  33834  baselsiga  34793  sigasspw  34794  ddeval1  34913  ddeval0  34914  braew  34921  derangen2  36025  subfaclim  36039  snmlff  36180  elfzm12  36526  fnetr  37231  wl-sbal1  38588  poimirlem13  38644  poimirlem14  38645  poimirlem31  38662  poimirlem32  38663  ismblfin  38672  itg2addnclem2  38683  areacirclem2  38720  areacirc  38724  ismgmOLD  38877  ismndo2  38901  rngomndo  38962  ecxrn2  39433  dmqseq  39749  prter3  40032  atbase  40439  llnbase  40659  lplnbase  40684  lvolbase  40728  lhpbase  41148  rernegcl  43515  renegadd  43516  reneg0addlid  43518  sn-0ne2  43550  3cubes  43793  mzpsubmpt  43847  mzpnegmpt  43848  eliunov2  44772  iunrelexp0  44795  enmappwid  45093  uunT1  45855  nnfoctb  46158  rn1st  46378  afveu  48316  afv2eu  48401  afv20fv0  48426  fzopredsuc  48487  fargshiftfva  48618  lindsrng01  49673  cic1st2nd  50254  cicpropdlem  50256  zeroo2  50449