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  3836  csbie2df  4396  xpiindi  5782  fununfun  6534  dffv2  6922  elunirn2OLD  7193  fliftcnv  7252  riotaprop  7337  elovmpt3rab1  7613  3xpexg  7692  orduniorsuc  7769  unielxp  7969  dmtpos  8178  tpossym  8198  oesuclem  8450  ercnv  8653  cnvct  8966  sucxpdom  9160  enp1i  9182  pwfilem  9225  3xpfi  9229  rankr1id  9777  cardnn  9878  alephnbtwn2  9985  alephsucdom  9992  cdainflem  10101  isfin4p1  10228  axcclem  10370  dmct  10437  mptct  10451  infxpidm  10475  fpwwe2lem8  10551  gchpwdom  10583  elwina  10599  elina  10600  rankcf  10690  ltexprlem4  10952  lem1  11985  ltdivp1i  12069  nn0le2x  12456  rpnnen1lem5  12900  eluzfz1  13452  fzpred  13493  uznfz  13531  fz0fzdiffz0  13558  fzctr  13561  flid  13730  modid0  13819  2txmodxeq0  13856  faclbnd3  14217  faclbnd4lem4  14221  bcn1  14238  hashfac  14383  repswsymballbi  14704  wrdlen2i  14867  dfrtrclrec2  14983  rtrclreclem3  14985  rtrclreclem4  14986  relexpindlem  14988  sqrtsq  15194  absrdbnd  15267  sqreulem  15285  sqreu  15286  bpoly2  15982  bpoly3  15983  gcd0id  16448  lcmgcdlem  16535  lcmftp  16565  dvdsnprmd  16619  2mulprm  16622  pcprod  16825  fldivp1  16827  invsym2  17688  pleval2i  18258  smndlsmidm  19553  gsumle  20042  subrgsubm  20488  resrhm2b  20505  cncrngOLD  21314  pzriprnglem11  21416  znchr  21487  psrbagfsupp  21844  mattposvs  22358  smadiadetglem2  22575  tg1  22867  cldval  22926  cldss  22932  cldopn  22934  1stcrestlem  23355  refbas  23413  refssex  23414  regr1  23653  kqreg  23654  kqnrm  23655  ufilen  23833  efmndtmd  24004  symgtgp  24009  psmetdmdm  24209  icoopnst  24852  cnheiborlem  24869  cfilfcls  25190  eflogeq  26527  logdivlt  26546  logdifbnd  26920  harmonicbnd4  26937  basellem5  27011  bposlem7  27217  zabsle1  27223  addsqn2reu  27368  chto1ub  27403  chpo1ub  27407  vmadivsum  27409  dchrmusum2  27421  dchrvmasum2if  27424  dchrvmasumlema  27427  dchrvmasumiflem2  27429  dchrisum0re  27440  dchrvmasumlem  27450  rplogsum  27454  mulogsumlem  27458  logdivsum  27460  selberg2lem  27477  pntrmax  27491  pntlem3  27536  pntleml  27538  pnt2  27540  noextendlt  27597  usgredg2vlem2  29189  vtxdgelxnn0  29436  wlkonprop  29620  wksonproplem  29666  wwlknbp  29805  wspthnp  29813  wlklnwwlkln1  29831  clwwlkf  30009  erclwwlknsym  30032  erclwwlkntr  30033  eupth0  30176  numclwwlk1lem2fo  30320  numclwlk2lem2f  30339  numclwwlk5lem  30349  hilablo  31122  hhssabloilem  31223  mayete3i  31690  homullid  31762  adjeu  31851  lnopeqi  31970  cnlnadjlem7  32035  adjbdlnb  32046  nmopcoadji  32063  bracnlnval  32076  mptctf  32674  xraddge02  32713  xrge0npcan  32987  gsumvsca1  33181  gsumvsca2  33182  baselsiga  34084  sigasspw  34085  ddeval1  34203  ddeval0  34204  braew  34211  derangen2  35149  subfaclim  35163  snmlff  35304  elfzm12  35650  fnetr  36327  wl-sbal1  37539  poimirlem13  37615  poimirlem14  37616  poimirlem31  37633  poimirlem32  37634  ismblfin  37643  itg2addnclem2  37654  areacirclem2  37691  areacirc  37695  ismgmOLD  37832  ismndo2  37856  rngomndo  37917  dmqseq  38619  prter3  38863  atbase  39270  llnbase  39491  lplnbase  39516  lvolbase  39560  lhpbase  39980  rernegcl  42347  renegadd  42348  reneg0addlid  42350  sn-0ne2  42382  3cubes  42666  mzpsubmpt  42719  mzpnegmpt  42720  eliunov2  43655  iunrelexp0  43678  enmappwid  43976  uunT1  44756  nnfoctb  45029  rn1st  45254  afveu  47141  afv2eu  47226  afv20fv0  47251  fzopredsuc  47311  fargshiftfva  47431  lindsrng01  48457  cic1st2nd  49036  cicpropdlem  49038  zeroo2  49223