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  3862  csbie2df  4423  xpiindi  5820  fununfun  6589  dffv2  6979  elunirn2OLD  7250  fliftcnv  7309  riotaprop  7394  elovmpt3rab1  7672  3xpexg  7751  orduniorsuc  7829  unielxp  8031  dmtpos  8242  tpossym  8262  wfrlem5OLD  8332  oesuclem  8542  ercnv  8745  cnvct  9053  undomOLD  9079  sucxpdom  9268  enp1i  9290  pwfilem  9333  3xpfi  9337  rankr1id  9881  cardnn  9982  alephnbtwn2  10091  alephsucdom  10098  cdainflem  10207  isfin4p1  10334  axcclem  10476  dmct  10543  mptct  10557  infxpidm  10581  fpwwe2lem8  10657  gchpwdom  10689  elwina  10705  elina  10706  rankcf  10796  ltexprlem4  11058  lem1  12089  ltdivp1i  12173  nn0le2x  12560  rpnnen1lem5  13002  eluzfz1  13553  fzpred  13594  uznfz  13632  fz0fzdiffz0  13659  fzctr  13662  flid  13830  modid0  13919  2txmodxeq0  13954  faclbnd3  14315  faclbnd4lem4  14319  bcn1  14336  hashfac  14481  repswsymballbi  14803  wrdlen2i  14966  dfrtrclrec2  15082  rtrclreclem3  15084  rtrclreclem4  15085  relexpindlem  15087  sqrtsq  15293  absrdbnd  15365  sqreulem  15383  sqreu  15384  bpoly2  16078  bpoly3  16079  gcd0id  16543  lcmgcdlem  16630  lcmftp  16660  dvdsnprmd  16714  2mulprm  16717  pcprod  16920  fldivp1  16922  invsym2  17781  pleval2i  18351  smndlsmidm  19642  subrgsubm  20550  resrhm2b  20567  cncrngOLD  21357  pzriprnglem11  21457  znchr  21528  psrbagfsupp  21884  mattposvs  22398  smadiadetglem2  22615  tg1  22907  cldval  22966  cldss  22972  cldopn  22974  1stcrestlem  23395  refbas  23453  refssex  23454  regr1  23693  kqreg  23694  kqnrm  23695  ufilen  23873  efmndtmd  24044  symgtgp  24049  psmetdmdm  24249  icoopnst  24892  cnheiborlem  24909  cfilfcls  25231  eflogeq  26568  logdivlt  26587  logdifbnd  26961  harmonicbnd4  26978  basellem5  27052  bposlem7  27258  zabsle1  27264  addsqn2reu  27409  chto1ub  27444  chpo1ub  27448  vmadivsum  27450  dchrmusum2  27462  dchrvmasum2if  27465  dchrvmasumlema  27468  dchrvmasumiflem2  27470  dchrisum0re  27481  dchrvmasumlem  27491  rplogsum  27495  mulogsumlem  27499  logdivsum  27501  selberg2lem  27518  pntrmax  27532  pntlem3  27577  pntleml  27579  pnt2  27581  noextendlt  27638  usgredg2vlem2  29210  vtxdgelxnn0  29457  wlkonprop  29643  wksonproplem  29689  wksonproplemOLD  29690  wwlknbp  29829  wspthnp  29837  wlklnwwlkln1  29855  clwwlkf  30033  erclwwlknsym  30056  erclwwlkntr  30057  eupth0  30200  numclwwlk1lem2fo  30344  numclwlk2lem2f  30363  numclwwlk5lem  30373  hilablo  31146  hhssabloilem  31247  mayete3i  31714  homullid  31786  adjeu  31875  lnopeqi  31994  cnlnadjlem7  32059  adjbdlnb  32070  nmopcoadji  32087  bracnlnval  32100  mptctf  32700  xraddge02  32739  xrge0npcan  33020  gsumle  33097  gsumvsca1  33228  gsumvsca2  33229  baselsiga  34151  sigasspw  34152  ddeval1  34270  ddeval0  34271  braew  34278  derangen2  35201  subfaclim  35215  snmlff  35356  elfzm12  35702  fnetr  36374  wl-sbal1  37586  poimirlem13  37662  poimirlem14  37663  poimirlem31  37680  poimirlem32  37681  ismblfin  37690  itg2addnclem2  37701  areacirclem2  37738  areacirc  37742  ismgmOLD  37879  ismndo2  37903  rngomndo  37964  cnvepimaex  38359  dmqseq  38663  prter3  38905  atbase  39312  llnbase  39533  lplnbase  39558  lvolbase  39602  lhpbase  40022  rernegcl  42389  renegadd  42390  reneg0addlid  42392  sn-0ne2  42424  3cubes  42688  mzpsubmpt  42741  mzpnegmpt  42742  eliunov2  43678  iunrelexp0  43701  enmappwid  43999  uunT1  44779  nnfoctb  45052  rn1st  45277  afveu  47162  afv2eu  47247  afv20fv0  47272  fzopredsuc  47332  fargshiftfva  47437  lindsrng01  48424  cic1st2nd  48994  cicpropdlem  48996  zeroo2  49131