Theorem mpancom 686

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 586	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpan  688  spesbc  3865  csbie2df  4392  xpiindi  5701  fununfun  6397  dffv2  6751  fliftcnv  7058  riotaprop  7135  elovmpt3rab1  7399  3xpexg  7469  orduniorsuc  7539  unielxp  7721  dmtpos  7898  tpossym  7918  wfrlem5  7953  oesuclem  8144  ercnv  8304  cnvct  8580  undom  8599  sucxpdom  8721  3xpfi  8784  pwfilem  8812  rankr1id  9285  cardnn  9386  alephnbtwn2  9492  alephsucdom  9499  cdainflem  9607  isfin4p1  9731  axcclem  9873  dmct  9940  mptct  9954  infxpidm  9978  fpwwe2lem9  10054  gchpwdom  10086  elwina  10102  elina  10103  rankcf  10193  ltexprlem4  10455  lem1  11477  ltdivp1i  11560  rpnnen1lem5  12374  eluzfz1  12908  fzpred  12949  uznfz  12984  fz0fzdiffz0  13010  fzctr  13013  flid  13172  modid0  13259  2txmodxeq0  13293  faclbnd3  13646  faclbnd4lem4  13650  bcn1  13667  hashfac  13810  repswsymballbi  14136  wrdlen2i  14298  dfrtrclrec2  14410  rtrclreclem3  14413  rtrclreclem4  14414  relexpindlem  14416  sqrtsq  14623  absrdbnd  14695  sqreulem  14713  sqreu  14714  bpoly2  15405  bpoly3  15406  gcd0id  15861  lcmgcdlem  15944  lcmftp  15974  dvdsnprmd  16028  2mulprm  16031  pcprod  16225  fldivp1  16227  invsym2  17027  pleval2i  17568  smndlsmidm  18775  subrgsubm  19542  cncrng  20560  znchr  20703  mattposvs  21058  smadiadetglem2  21275  tg1  21566  cldval  21625  cldss  21631  cldopn  21633  1stcrestlem  22054  refbas  22112  refssex  22113  regr1  22352  kqreg  22353  kqnrm  22354  ufilen  22532  efmndtmd  22703  symgtgp  22708  elrnust  22827  psmetdmdm  22909  metuval  23153  icoopnst  23537  cnheiborlem  23552  cfilfcls  23871  eflogeq  25179  logdivlt  25198  logdifbnd  25565  harmonicbnd4  25582  basellem5  25656  bposlem7  25860  zabsle1  25866  addsqn2reu  26011  chto1ub  26046  chpo1ub  26050  vmadivsum  26052  dchrmusum2  26064  dchrvmasum2if  26067  dchrvmasumlema  26070  dchrvmasumiflem2  26072  dchrisum0re  26083  dchrvmasumlem  26093  rplogsum  26097  mulogsumlem  26101  logdivsum  26103  selberg2lem  26120  pntrmax  26134  pntlem3  26179  pntleml  26181  pnt2  26183  usgredg2vlem2  27002  vtxdgelxnn0  27248  wlkonprop  27434  wksonproplem  27480  wwlknbp  27614  wspthnp  27622  wlklnwwlkln1  27640  clwwlkf  27820  erclwwlknsym  27843  erclwwlkntr  27844  eupth0  27987  numclwwlk1lem2fo  28131  numclwlk2lem2f  28150  numclwwlk5lem  28160  hilablo  28931  hhssabloilem  29032  mayete3i  29499  homulid2  29571  adjeu  29660  lnopeqi  29779  cnlnadjlem7  29844  adjbdlnb  29855  nmopcoadji  29872  bracnlnval  29885  elunirn2  30390  mptctf  30447  xraddge02  30474  xrge0npcan  30676  gsumle  30720  gsumvsca1  30849  gsumvsca2  30850  metidval  31125  pstmval  31130  baselsiga  31369  sigasspw  31370  ddeval1  31488  ddeval0  31489  braew  31496  derangen2  32416  subfaclim  32430  snmlff  32571  elfzm12  32913  noextendlt  33171  fnetr  33694  wl-sbal1  34793  poimirlem13  34899  poimirlem14  34900  poimirlem31  34917  poimirlem32  34918  ismblfin  34927  itg2addnclem2  34938  areacirclem2  34977  areacirc  34981  ismgmOLD  35122  ismndo2  35146  rngomndo  35207  cnvepimaex  35587  dmqseq  35869  prter3  36012  atbase  36419  llnbase  36639  lplnbase  36664  lvolbase  36708  lhpbase  37128  rernegcl  39194  renegadd  39195  reneg0addid2  39197  sn-0ne2  39229  3cubes  39280  mzpsubmpt  39333  mzpnegmpt  39334  eliunov2  40017  iunrelexp0  40040  enmappwid  40339  uunT1  41107  nnfoctb  41302  afveu  43345  afv2eu  43430  afv20fv0  43455  fzopredsuc  43516  fargshiftfva  43596  lindsrng01  44516