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  3829  csbie2df  4401  xpiindi  5812  fununfun  6580  dffv2  6972  fliftcnv  7311  riotaprop  7396  elovmpt3rab1  7673  3xpexg  7755  orduniorsuc  7830  unielxp  8028  dmtpos  8239  tpossym  8259  oesuclem  8517  ercnv  8723  cnvct  9046  sucxpdom  9236  enp1i  9254  pwfilem  9293  3xpfi  9296  rankr1id  9859  cardnn  10025  alephnbtwn2  10132  alephsucdom  10139  cdainflem  10247  isfin4p1  10374  axcclem  10516  dmct  10583  dmctOLD  10584  mptct  10603  infxpidm  10627  fpwwe2lem8  10704  gchpwdom  10736  elwina  10752  elina  10753  rankcf  10843  ltexprlem4  11105  lem1  12141  ltdivp1i  12224  nn0le2x  12641  rpnnen1lem5  13090  eluzfz1  13644  fzpred  13686  uznfz  13724  fz0fzdiffz0  13751  fzctr  13754  flid  13928  modid0  14017  2txmodxeq0  14054  faclbnd3  14416  faclbnd4lem4  14420  bcn1  14437  hashfac  14583  repswsymballbi  14911  wrdlen2i  15073  dfrtrclrec2  15191  rtrclreclem3  15193  rtrclreclem4  15194  relexpindlem  15196  sqrtsq  15416  absrdbnd  15489  sqreulem  15507  sqreu  15508  bpoly2  16203  bpoly3  16204  gcd0id  16671  lcmgcdlem  16761  lcmftp  16791  dvdsnprmd  16845  2mulprm  16848  pcprod  17053  fldivp1  17055  invsym2  17918  pleval2i  18488  smndlsmidm  19850  gsumle  20339  subrgsubm  20817  resrhm2b  20834  pzriprnglem11  21777  znchr  21848  psrbagfsupp  22207  mattposvs  22750  smadiadetglem2  22967  tg1  23262  cldval  23321  cldss  23327  cldopn  23329  1stcrestlem  23750  refbas  23809  refssex  23810  regr1  24049  kqreg  24050  kqnrm  24051  ufilen  24229  efmndtmd  24400  symgtgp  24405  psmetdmdm  24604  icoopnst  25240  cnheiborlem  25255  cfilfcls  25575  eflogeq  26912  logdivlt  26931  logdifbnd  27303  harmonicbnd4  27320  basellem5  27394  bposlem7  27599  zabsle1  27605  addsqn2reu  27750  chto1ub  27785  chpo1ub  27789  vmadivsum  27791  dchrmusum2  27803  dchrvmasum2if  27806  dchrvmasumlema  27809  dchrvmasumiflem2  27811  dchrisum0re  27822  dchrvmasumlem  27832  rplogsum  27836  mulogsumlem  27840  logdivsum  27842  selberg2lem  27859  pntrmax  27873  pntlem3  27918  pntleml  27920  pnt2  27922  noextendlt  28008  usgredg2vlem2  29789  vtxdgelxnn0  30035  wlkonprop  30219  wksonproplem  30269  wwlknbp  30413  wspthnp  30421  wlklnwwlkln1  30439  clwwlkf  30620  erclwwlknsym  30643  erclwwlkntr  30644  eupth0  30797  numclwwlk1lem2fo  30941  numclwlk2lem2f  30960  numclwwlk5lem  30970  hilablo  31744  hhssabloilem  31845  mayete3i  32312  homullid  32384  adjeu  32473  lnopeqi  32592  cnlnadjlem7  32657  adjbdlnb  32668  nmopcoadji  32685  bracnlnval  32698  mptctf  33290  xraddge02  33331  xrge0npcan  33563  gsumvsca1  33769  gsumvsca2  33770  baselsiga  34729  sigasspw  34730  ddeval1  34849  ddeval0  34850  braew  34857  derangen2  35908  subfaclim  35922  snmlff  36063  elfzm12  36409  fnetr  37109  wl-sbal1  38463  poimirlem13  38519  poimirlem14  38520  poimirlem31  38537  poimirlem32  38538  ismblfin  38547  itg2addnclem2  38558  areacirclem2  38595  areacirc  38599  ismgmOLD  38752  ismndo2  38776  rngomndo  38837  ecxrn2  39308  dmqseq  39624  prter3  39907  atbase  40314  llnbase  40534  lplnbase  40559  lvolbase  40603  lhpbase  41023  rernegcl  43390  renegadd  43391  reneg0addlid  43393  sn-0ne2  43425  3cubes  43654  mzpsubmpt  43707  mzpnegmpt  43708  eliunov2  44638  iunrelexp0  44661  enmappwid  44959  uunT1  45721  nnfoctb  46008  rn1st  46228  afveu  48167  afv2eu  48252  afv20fv0  48277  fzopredsuc  48338  fargshiftfva  48469  lindsrng01  49524  cic1st2nd  50099  cicpropdlem  50101  zeroo2  50286