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  3832  csbie2df  4404  xpiindi  5819  fununfun  6585  dffv2  6977  fliftcnv  7316  riotaprop  7401  elovmpt3rab1  7678  3xpexg  7755  orduniorsuc  7830  unielxp  8028  dmtpos  8240  tpossym  8260  oesuclem  8516  ercnv  8722  cnvct  9045  sucxpdom  9235  enp1i  9253  pwfilem  9291  3xpfi  9294  rankr1id  9848  cardnn  9972  alephnbtwn2  10079  alephsucdom  10086  cdainflem  10194  isfin4p1  10321  axcclem  10463  dmct  10530  dmctOLD  10531  mptct  10550  infxpidm  10574  fpwwe2lem8  10651  gchpwdom  10683  elwina  10699  elina  10700  rankcf  10790  ltexprlem4  11052  lem1  12086  ltdivp1i  12169  nn0le2x  12586  rpnnen1lem5  13035  eluzfz1  13589  fzpred  13631  uznfz  13669  fz0fzdiffz0  13696  fzctr  13699  flid  13873  modid0  13962  2txmodxeq0  13999  faclbnd3  14360  faclbnd4lem4  14364  bcn1  14381  hashfac  14527  repswsymballbi  14855  wrdlen2i  15017  dfrtrclrec2  15135  rtrclreclem3  15137  rtrclreclem4  15138  relexpindlem  15140  sqrtsq  15360  absrdbnd  15433  sqreulem  15451  sqreu  15452  bpoly2  16149  bpoly3  16150  gcd0id  16615  lcmgcdlem  16702  lcmftp  16732  dvdsnprmd  16786  2mulprm  16789  pcprod  16993  fldivp1  16995  invsym2  17858  pleval2i  18428  smndlsmidm  19789  gsumle  20278  subrgsubm  20753  resrhm2b  20770  pzriprnglem11  21710  znchr  21781  psrbagfsupp  22140  mattposvs  22683  smadiadetglem2  22900  tg1  23195  cldval  23254  cldss  23260  cldopn  23262  1stcrestlem  23683  refbas  23742  refssex  23743  regr1  23982  kqreg  23983  kqnrm  23984  ufilen  24162  efmndtmd  24333  symgtgp  24338  psmetdmdm  24537  icoopnst  25173  cnheiborlem  25188  cfilfcls  25508  eflogeq  26847  logdivlt  26866  logdifbnd  27238  harmonicbnd4  27255  basellem5  27329  bposlem7  27534  zabsle1  27540  addsqn2reu  27685  chto1ub  27720  chpo1ub  27724  vmadivsum  27726  dchrmusum2  27738  dchrvmasum2if  27741  dchrvmasumlema  27744  dchrvmasumiflem2  27746  dchrisum0re  27757  dchrvmasumlem  27767  rplogsum  27771  mulogsumlem  27775  logdivsum  27777  selberg2lem  27794  pntrmax  27808  pntlem3  27853  pntleml  27855  pnt2  27857  noextendlt  27913  usgredg2vlem2  29694  vtxdgelxnn0  29940  wlkonprop  30124  wksonproplem  30174  wwlknbp  30318  wspthnp  30326  wlklnwwlkln1  30344  clwwlkf  30525  erclwwlknsym  30548  erclwwlkntr  30549  eupth0  30702  numclwwlk1lem2fo  30846  numclwlk2lem2f  30865  numclwwlk5lem  30875  hilablo  31649  hhssabloilem  31750  mayete3i  32217  homullid  32289  adjeu  32378  lnopeqi  32497  cnlnadjlem7  32562  adjbdlnb  32573  nmopcoadji  32590  bracnlnval  32603  mptctf  33195  xraddge02  33236  xrge0npcan  33468  gsumvsca1  33674  gsumvsca2  33675  baselsiga  34633  sigasspw  34634  ddeval1  34753  ddeval0  34754  braew  34761  derangen2  35761  subfaclim  35775  snmlff  35916  elfzm12  36262  fnetr  36978  wl-sbal1  38334  poimirlem13  38390  poimirlem14  38391  poimirlem31  38408  poimirlem32  38409  ismblfin  38418  itg2addnclem2  38429  areacirclem2  38466  areacirc  38470  ismgmOLD  38608  ismndo2  38632  rngomndo  38693  ecxrn2  39164  dmqseq  39480  prter3  39763  atbase  40170  llnbase  40390  lplnbase  40415  lvolbase  40459  lhpbase  40879  rernegcl  43254  renegadd  43255  reneg0addlid  43257  sn-0ne2  43289  3cubes  43543  mzpsubmpt  43596  mzpnegmpt  43597  eliunov2  44527  iunrelexp0  44550  enmappwid  44848  uunT1  45610  nnfoctb  45890  rn1st  46110  afveu  48049  afv2eu  48134  afv20fv0  48159  fzopredsuc  48220  fargshiftfva  48351  lindsrng01  49406  cic1st2nd  49981  cicpropdlem  49983  zeroo2  50168