Theorem mpancom 687

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 583	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  689  spesbc  3904  csbie2df  4466  xpiindi  5860  fununfun  6626  dffv2  7017  elunirn2OLD  7290  fliftcnv  7347  riotaprop  7432  elovmpt3rab1  7710  3xpexg  7787  orduniorsuc  7866  unielxp  8068  dmtpos  8279  tpossym  8299  wfrlem5OLD  8369  oesuclem  8581  ercnv  8784  cnvct  9099  undomOLD  9126  sucxpdom  9318  enp1i  9341  pwfilem  9384  3xpfi  9388  pwfilemOLD  9416  rankr1id  9931  cardnn  10032  alephnbtwn2  10141  alephsucdom  10148  cdainflem  10257  isfin4p1  10384  axcclem  10526  dmct  10593  mptct  10607  infxpidm  10631  fpwwe2lem8  10707  gchpwdom  10739  elwina  10755  elina  10756  rankcf  10846  ltexprlem4  11108  lem1  12137  ltdivp1i  12221  rpnnen1lem5  13046  eluzfz1  13591  fzpred  13632  uznfz  13667  fz0fzdiffz0  13694  fzctr  13697  flid  13859  modid0  13948  2txmodxeq0  13982  faclbnd3  14341  faclbnd4lem4  14345  bcn1  14362  hashfac  14507  repswsymballbi  14828  wrdlen2i  14991  dfrtrclrec2  15107  rtrclreclem3  15109  rtrclreclem4  15110  relexpindlem  15112  sqrtsq  15318  absrdbnd  15390  sqreulem  15408  sqreu  15409  bpoly2  16105  bpoly3  16106  gcd0id  16565  lcmgcdlem  16653  lcmftp  16683  dvdsnprmd  16737  2mulprm  16740  pcprod  16942  fldivp1  16944  invsym2  17824  pleval2i  18406  smndlsmidm  19698  subrgsubm  20613  resrhm2b  20630  cncrngOLD  21425  pzriprnglem11  21525  znchr  21604  psrbagfsupp  21962  mattposvs  22482  smadiadetglem2  22699  tg1  22992  cldval  23052  cldss  23058  cldopn  23060  1stcrestlem  23481  refbas  23539  refssex  23540  regr1  23779  kqreg  23780  kqnrm  23781  ufilen  23959  efmndtmd  24130  symgtgp  24135  psmetdmdm  24336  icoopnst  24988  cnheiborlem  25005  cfilfcls  25327  eflogeq  26662  logdivlt  26681  logdifbnd  27055  harmonicbnd4  27072  basellem5  27146  bposlem7  27352  zabsle1  27358  addsqn2reu  27503  chto1ub  27538  chpo1ub  27542  vmadivsum  27544  dchrmusum2  27556  dchrvmasum2if  27559  dchrvmasumlema  27562  dchrvmasumiflem2  27564  dchrisum0re  27575  dchrvmasumlem  27585  rplogsum  27589  mulogsumlem  27593  logdivsum  27595  selberg2lem  27612  pntrmax  27626  pntlem3  27671  pntleml  27673  pnt2  27675  noextendlt  27732  usgredg2vlem2  29261  vtxdgelxnn0  29508  wlkonprop  29694  wksonproplem  29740  wksonproplemOLD  29741  wwlknbp  29875  wspthnp  29883  wlklnwwlkln1  29901  clwwlkf  30079  erclwwlknsym  30102  erclwwlkntr  30103  eupth0  30246  numclwwlk1lem2fo  30390  numclwlk2lem2f  30409  numclwwlk5lem  30419  hilablo  31192  hhssabloilem  31293  mayete3i  31760  homullid  31832  adjeu  31921  lnopeqi  32040  cnlnadjlem7  32105  adjbdlnb  32116  nmopcoadji  32133  bracnlnval  32146  mptctf  32731  xraddge02  32763  xrge0npcan  33006  gsumle  33074  gsumvsca1  33205  gsumvsca2  33206  baselsiga  34079  sigasspw  34080  ddeval1  34198  ddeval0  34199  braew  34206  derangen2  35142  subfaclim  35156  snmlff  35297  elfzm12  35643  fnetr  36317  wl-sbal1  37517  poimirlem13  37593  poimirlem14  37594  poimirlem31  37611  poimirlem32  37612  ismblfin  37621  itg2addnclem2  37632  areacirclem2  37669  areacirc  37673  ismgmOLD  37810  ismndo2  37834  rngomndo  37895  cnvepimaex  38292  dmqseq  38596  prter3  38838  atbase  39245  llnbase  39466  lplnbase  39491  lvolbase  39535  lhpbase  39955  rernegcl  42347  renegadd  42348  reneg0addlid  42350  sn-0ne2  42382  3cubes  42646  mzpsubmpt  42699  mzpnegmpt  42700  eliunov2  43641  iunrelexp0  43664  enmappwid  43962  uunT1  44751  nnfoctb  44949  rn1st  45183  afveu  47068  afv2eu  47153  afv20fv0  47178  fzopredsuc  47238  fargshiftfva  47317  lindsrng01  48197