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  3833  csbie2df  4404  xpiindi  5819  iotan0  6550  fununfunOLD  6612  dffv2  7006  fliftcnv  7345  riotaprop  7430  elovmpt3rab1  7708  3xpexg  7793  orduniorsuc  7868  unielxp  8066  dmtpos  8286  tpossym  8306  oesuclem  8564  ercnv  8770  cnvct  9093  sucxpdom  9283  enp1i  9301  pwfilem  9340  3xpfi  9343  rankr1id  9908  cardnn  10074  alephnbtwn2  10181  alephsucdom  10188  cdainflem  10296  isfin4p1  10423  axcclem  10565  dmct  10632  dmctOLD  10633  mptct  10652  infxpidm  10676  fpwwe2lem8  10753  gchpwdom  10785  elwina  10801  elina  10802  rankcf  10892  ltexprlem4  11154  lem1  12190  ltdivp1i  12273  nn0le2x  12690  rpnnen1lem5  13139  eluzfz1  13694  fzpred  13736  uznfz  13774  fz0fzdiffz0  13801  flid  13978  modid0  14067  2txmodxeq0  14104  faclbnd3  14466  faclbnd4lem4  14470  bcn1  14487  hashfac  14633  repswsymballbi  14962  wrdlen2i  15125  dfrtrclrec2  15243  rtrclreclem3  15245  rtrclreclem4  15246  relexpindlem  15248  sqrtsq  15468  absrdbnd  15541  sqreulem  15559  sqreu  15560  bpoly2  16255  bpoly3  16256  gcd0id  16723  lcmgcdlem  16813  lcmftp  16843  dvdsnprmd  16897  2mulprm  16900  pcprod  17105  fldivp1  17107  invsym2  17970  pleval2i  18540  smndlsmidm  19903  gsumle  20392  subrgsubm  20870  resrhm2b  20887  pzriprnglem11  21830  znchr  21901  psrbagfsupp  22260  mattposvs  22803  smadiadetglem2  23020  tg1  23315  cldval  23374  cldss  23380  cldopn  23382  1stcrestlem  23803  refbas  23862  refssex  23863  regr1  24102  kqreg  24103  kqnrm  24104  ufilen  24282  efmndtmd  24453  symgtgp  24458  psmetdmdm  24657  icoopnst  25293  cnheiborlem  25308  cfilfcls  25628  eflogeq  26963  logdivlt  26982  logdifbnd  27354  harmonicbnd4  27371  basellem5  27445  bposlem7  27650  zabsle1  27656  addsqn2reu  27801  chto1ub  27836  chpo1ub  27840  vmadivsum  27842  dchrmusum2  27854  dchrvmasum2if  27857  dchrvmasumlema  27860  dchrvmasumiflem2  27862  dchrisum0re  27873  dchrvmasumlem  27883  rplogsum  27887  mulogsumlem  27891  logdivsum  27893  selberg2lem  27910  pntrmax  27924  pntlem3  27969  pntleml  27971  pnt2  27973  noextendlt  28059  usgredg2vlem2  29840  vtxdgelxnn0  30086  wlkonprop  30270  wksonproplem  30320  wwlknbp  30464  wspthnp  30472  wlklnwwlkln1  30490  clwwlkf  30671  erclwwlknsym  30694  erclwwlkntr  30695  eupth0  30848  numclwwlk1lem2fo  30992  numclwlk2lem2f  31011  numclwwlk5lem  31021  hilablo  31795  hhssabloilem  31896  mayete3i  32363  homullid  32435  adjeu  32524  lnopeqi  32643  cnlnadjlem7  32708  adjbdlnb  32719  nmopcoadji  32736  bracnlnval  32749  mptctf  33382  xraddge02  33422  xrge0npcan  33657  gsumvsca1  33863  gsumvsca2  33864  baselsiga  34830  sigasspw  34831  ddeval1  34950  ddeval0  34951  braew  34958  jk1k2k3  36031  derangen2  36119  subfaclim  36133  snmlff  36274  elfzm12  36620  fnetr  37330  wl-sbal1  38700  poimirlem13  38756  poimirlem14  38757  poimirlem31  38774  poimirlem32  38775  ismblfin  38784  itg2addnclem2  38795  areacirclem2  38832  areacirc  38836  ismgmOLD  38987  ismndo2  39011  rngomndo  39072  ecxrn2  39543  dmqseq  39859  prter3  40142  atbase  40549  llnbase  40769  lplnbase  40794  lvolbase  40838  lhpbase  41258  rernegcl  43626  renegadd  43627  reneg0addlid  43629  sn-0ne2  43661  3cubes  43904  mzpsubmpt  43958  mzpnegmpt  43959  eliunov2  44882  iunrelexp0  44905  enmappwid  45203  uunT1  45964  nnfoctb  46281  rn1st  46500  afveu  48438  afv2eu  48523  afv20fv0  48548  fzopredsuc  48609  fargshiftfva  48740  lindsrng01  49795  cic1st2nd  50376  cicpropdlem  50378  zeroo2  50571