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  3891  csbie2df  4449  xpiindi  5849  fununfun  6616  dffv2  7004  elunirn2OLD  7273  fliftcnv  7331  riotaprop  7415  elovmpt3rab1  7693  3xpexg  7771  orduniorsuc  7850  unielxp  8051  dmtpos  8262  tpossym  8282  wfrlem5OLD  8352  oesuclem  8562  ercnv  8765  cnvct  9073  undomOLD  9099  sucxpdom  9289  enp1i  9311  pwfilem  9354  3xpfi  9358  rankr1id  9900  cardnn  10001  alephnbtwn2  10110  alephsucdom  10117  cdainflem  10226  isfin4p1  10353  axcclem  10495  dmct  10562  mptct  10576  infxpidm  10600  fpwwe2lem8  10676  gchpwdom  10708  elwina  10724  elina  10725  rankcf  10815  ltexprlem4  11077  lem1  12108  ltdivp1i  12192  nn0le2x  12578  rpnnen1lem5  13021  eluzfz1  13568  fzpred  13609  uznfz  13647  fz0fzdiffz0  13674  fzctr  13677  flid  13845  modid0  13934  2txmodxeq0  13969  faclbnd3  14328  faclbnd4lem4  14332  bcn1  14349  hashfac  14494  repswsymballbi  14815  wrdlen2i  14978  dfrtrclrec2  15094  rtrclreclem3  15096  rtrclreclem4  15097  relexpindlem  15099  sqrtsq  15305  absrdbnd  15377  sqreulem  15395  sqreu  15396  bpoly2  16090  bpoly3  16091  gcd0id  16553  lcmgcdlem  16640  lcmftp  16670  dvdsnprmd  16724  2mulprm  16727  pcprod  16929  fldivp1  16931  invsym2  17811  pleval2i  18394  smndlsmidm  19689  subrgsubm  20602  resrhm2b  20619  cncrngOLD  21420  pzriprnglem11  21520  znchr  21599  psrbagfsupp  21957  mattposvs  22477  smadiadetglem2  22694  tg1  22987  cldval  23047  cldss  23053  cldopn  23055  1stcrestlem  23476  refbas  23534  refssex  23535  regr1  23774  kqreg  23775  kqnrm  23776  ufilen  23954  efmndtmd  24125  symgtgp  24130  psmetdmdm  24331  icoopnst  24983  cnheiborlem  25000  cfilfcls  25322  eflogeq  26659  logdivlt  26678  logdifbnd  27052  harmonicbnd4  27069  basellem5  27143  bposlem7  27349  zabsle1  27355  addsqn2reu  27500  chto1ub  27535  chpo1ub  27539  vmadivsum  27541  dchrmusum2  27553  dchrvmasum2if  27556  dchrvmasumlema  27559  dchrvmasumiflem2  27561  dchrisum0re  27572  dchrvmasumlem  27582  rplogsum  27586  mulogsumlem  27590  logdivsum  27592  selberg2lem  27609  pntrmax  27623  pntlem3  27668  pntleml  27670  pnt2  27672  noextendlt  27729  usgredg2vlem2  29258  vtxdgelxnn0  29505  wlkonprop  29691  wksonproplem  29737  wksonproplemOLD  29738  wwlknbp  29872  wspthnp  29880  wlklnwwlkln1  29898  clwwlkf  30076  erclwwlknsym  30099  erclwwlkntr  30100  eupth0  30243  numclwwlk1lem2fo  30387  numclwlk2lem2f  30406  numclwwlk5lem  30416  hilablo  31189  hhssabloilem  31290  mayete3i  31757  homullid  31829  adjeu  31918  lnopeqi  32037  cnlnadjlem7  32102  adjbdlnb  32113  nmopcoadji  32130  bracnlnval  32143  mptctf  32735  xraddge02  32767  xrge0npcan  33008  gsumle  33084  gsumvsca1  33215  gsumvsca2  33216  baselsiga  34096  sigasspw  34097  ddeval1  34215  ddeval0  34216  braew  34223  derangen2  35159  subfaclim  35173  snmlff  35314  elfzm12  35660  fnetr  36334  wl-sbal1  37544  poimirlem13  37620  poimirlem14  37621  poimirlem31  37638  poimirlem32  37639  ismblfin  37648  itg2addnclem2  37659  areacirclem2  37696  areacirc  37700  ismgmOLD  37837  ismndo2  37861  rngomndo  37922  cnvepimaex  38318  dmqseq  38622  prter3  38864  atbase  39271  llnbase  39492  lplnbase  39517  lvolbase  39561  lhpbase  39981  rernegcl  42378  renegadd  42379  reneg0addlid  42381  sn-0ne2  42413  3cubes  42678  mzpsubmpt  42731  mzpnegmpt  42732  eliunov2  43669  iunrelexp0  43692  enmappwid  43990  uunT1  44778  nnfoctb  44987  rn1st  45219  afveu  47103  afv2eu  47188  afv20fv0  47213  fzopredsuc  47273  fargshiftfva  47368  lindsrng01  48314