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  3829  csbie2df  4392  xpiindi  5781  fununfun  6536  dffv2  6925  fliftcnv  7253  riotaprop  7338  elovmpt3rab1  7614  3xpexg  7693  orduniorsuc  7768  unielxp  7967  dmtpos  8176  tpossym  8196  oesuclem  8448  ercnv  8651  cnvct  8965  sucxpdom  9154  enp1i  9172  pwfilem  9211  3xpfi  9214  rankr1id  9764  cardnn  9865  alephnbtwn2  9972  alephsucdom  9979  cdainflem  10088  isfin4p1  10215  axcclem  10357  dmct  10424  mptct  10438  infxpidm  10462  fpwwe2lem8  10538  gchpwdom  10570  elwina  10586  elina  10587  rankcf  10677  ltexprlem4  10939  lem1  11973  ltdivp1i  12057  nn0le2x  12444  rpnnen1lem5  12883  eluzfz1  13435  fzpred  13476  uznfz  13514  fz0fzdiffz0  13541  fzctr  13544  flid  13716  modid0  13805  2txmodxeq0  13842  faclbnd3  14203  faclbnd4lem4  14207  bcn1  14224  hashfac  14369  repswsymballbi  14691  wrdlen2i  14853  dfrtrclrec2  14969  rtrclreclem3  14971  rtrclreclem4  14972  relexpindlem  14974  sqrtsq  15180  absrdbnd  15253  sqreulem  15271  sqreu  15272  bpoly2  15968  bpoly3  15969  gcd0id  16434  lcmgcdlem  16521  lcmftp  16551  dvdsnprmd  16605  2mulprm  16608  pcprod  16811  fldivp1  16813  invsym2  17674  pleval2i  18244  smndlsmidm  19572  gsumle  20061  subrgsubm  20504  resrhm2b  20521  cncrngOLD  21330  pzriprnglem11  21432  znchr  21503  psrbagfsupp  21860  mattposvs  22373  smadiadetglem2  22590  tg1  22882  cldval  22941  cldss  22947  cldopn  22949  1stcrestlem  23370  refbas  23428  refssex  23429  regr1  23668  kqreg  23669  kqnrm  23670  ufilen  23848  efmndtmd  24019  symgtgp  24024  psmetdmdm  24223  icoopnst  24866  cnheiborlem  24883  cfilfcls  25204  eflogeq  26541  logdivlt  26560  logdifbnd  26934  harmonicbnd4  26951  basellem5  27025  bposlem7  27231  zabsle1  27237  addsqn2reu  27382  chto1ub  27417  chpo1ub  27421  vmadivsum  27423  dchrmusum2  27435  dchrvmasum2if  27438  dchrvmasumlema  27441  dchrvmasumiflem2  27443  dchrisum0re  27454  dchrvmasumlem  27464  rplogsum  27468  mulogsumlem  27472  logdivsum  27474  selberg2lem  27491  pntrmax  27505  pntlem3  27550  pntleml  27552  pnt2  27554  noextendlt  27611  usgredg2vlem2  29208  vtxdgelxnn0  29455  wlkonprop  29639  wksonproplem  29685  wwlknbp  29824  wspthnp  29832  wlklnwwlkln1  29850  clwwlkf  30031  erclwwlknsym  30054  erclwwlkntr  30055  eupth0  30198  numclwwlk1lem2fo  30342  numclwlk2lem2f  30361  numclwwlk5lem  30371  hilablo  31144  hhssabloilem  31245  mayete3i  31712  homullid  31784  adjeu  31873  lnopeqi  31992  cnlnadjlem7  32057  adjbdlnb  32068  nmopcoadji  32085  bracnlnval  32098  mptctf  32705  xraddge02  32746  xrge0npcan  33010  gsumvsca1  33204  gsumvsca2  33205  baselsiga  34151  sigasspw  34152  ddeval1  34270  ddeval0  34271  braew  34278  derangen2  35241  subfaclim  35255  snmlff  35396  elfzm12  35742  fnetr  36418  wl-sbal1  37630  poimirlem13  37696  poimirlem14  37697  poimirlem31  37714  poimirlem32  37715  ismblfin  37724  itg2addnclem2  37735  areacirclem2  37772  areacirc  37776  ismgmOLD  37913  ismndo2  37937  rngomndo  37998  ecxrn2  38455  dmqseq  38760  prter3  39004  atbase  39411  llnbase  39631  lplnbase  39656  lvolbase  39700  lhpbase  40120  rernegcl  42492  renegadd  42493  reneg0addlid  42495  sn-0ne2  42527  3cubes  42810  mzpsubmpt  42863  mzpnegmpt  42864  eliunov2  43799  iunrelexp0  43822  enmappwid  44120  uunT1  44899  nnfoctb  45172  rn1st  45397  afveu  47280  afv2eu  47365  afv20fv0  47390  fzopredsuc  47450  fargshiftfva  47570  lindsrng01  48596  cic1st2nd  49175  cicpropdlem  49177  zeroo2  49362