Theorem mpancom 685

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 206  df-an 396

This theorem is referenced by:  mpan  687  spesbc  3876  csbie2df  4440  xpiindi  5835  fununfun  6596  dffv2  6986  elunirn2OLD  7255  fliftcnv  7311  riotaprop  7396  elovmpt3rab1  7670  3xpexg  7743  orduniorsuc  7822  unielxp  8017  dmtpos  8229  tpossym  8249  wfrlem5OLD  8319  oesuclem  8531  ercnv  8730  cnvct  9040  undomOLD  9066  pwfilem  9183  sucxpdom  9261  enp1i  9285  3xpfi  9325  pwfilemOLD  9352  rankr1id  9863  cardnn  9964  alephnbtwn2  10073  alephsucdom  10080  cdainflem  10188  isfin4p1  10316  axcclem  10458  dmct  10525  mptct  10539  infxpidm  10563  fpwwe2lem8  10639  gchpwdom  10671  elwina  10687  elina  10688  rankcf  10778  ltexprlem4  11040  lem1  12064  ltdivp1i  12147  rpnnen1lem5  12972  eluzfz1  13515  fzpred  13556  uznfz  13591  fz0fzdiffz0  13617  fzctr  13620  flid  13780  modid0  13869  2txmodxeq0  13903  faclbnd3  14259  faclbnd4lem4  14263  bcn1  14280  hashfac  14426  repswsymballbi  14737  wrdlen2i  14900  dfrtrclrec2  15012  rtrclreclem3  15014  rtrclreclem4  15015  relexpindlem  15017  sqrtsq  15223  absrdbnd  15295  sqreulem  15313  sqreu  15314  bpoly2  16008  bpoly3  16009  gcd0id  16467  lcmgcdlem  16550  lcmftp  16580  dvdsnprmd  16634  2mulprm  16637  pcprod  16835  fldivp1  16837  invsym2  17717  pleval2i  18299  smndlsmidm  19572  subrgsubm  20483  resrhm2b  20500  cncrng  21255  pzriprnglem11  21351  znchr  21428  psrbagfsupp  21783  mattposvs  22277  smadiadetglem2  22494  tg1  22787  cldval  22847  cldss  22853  cldopn  22855  1stcrestlem  23276  refbas  23334  refssex  23335  regr1  23574  kqreg  23575  kqnrm  23576  ufilen  23754  efmndtmd  23925  symgtgp  23930  psmetdmdm  24131  icoopnst  24783  cnheiborlem  24800  cfilfcls  25122  eflogeq  26450  logdivlt  26469  logdifbnd  26840  harmonicbnd4  26857  basellem5  26931  bposlem7  27137  zabsle1  27143  addsqn2reu  27288  chto1ub  27323  chpo1ub  27327  vmadivsum  27329  dchrmusum2  27341  dchrvmasum2if  27344  dchrvmasumlema  27347  dchrvmasumiflem2  27349  dchrisum0re  27360  dchrvmasumlem  27370  rplogsum  27374  mulogsumlem  27378  logdivsum  27380  selberg2lem  27397  pntrmax  27411  pntlem3  27456  pntleml  27458  pnt2  27460  noextendlt  27516  usgredg2vlem2  28917  vtxdgelxnn0  29163  wlkonprop  29349  wksonproplem  29395  wksonproplemOLD  29396  wwlknbp  29530  wspthnp  29538  wlklnwwlkln1  29556  clwwlkf  29734  erclwwlknsym  29757  erclwwlkntr  29758  eupth0  29901  numclwwlk1lem2fo  30045  numclwlk2lem2f  30064  numclwwlk5lem  30074  hilablo  30847  hhssabloilem  30948  mayete3i  31415  homullid  31487  adjeu  31576  lnopeqi  31695  cnlnadjlem7  31760  adjbdlnb  31771  nmopcoadji  31788  bracnlnval  31801  mptctf  32376  xraddge02  32403  xrge0npcan  32629  gsumle  32679  gsumvsca1  32808  gsumvsca2  32809  baselsiga  33578  sigasspw  33579  ddeval1  33697  ddeval0  33698  braew  33705  derangen2  34630  subfaclim  34644  snmlff  34785  elfzm12  35125  gg-cncrng  35649  fnetr  35702  wl-sbal1  36894  poimirlem13  36967  poimirlem14  36968  poimirlem31  36985  poimirlem32  36986  ismblfin  36995  itg2addnclem2  37006  areacirclem2  37043  areacirc  37047  ismgmOLD  37184  ismndo2  37208  rngomndo  37269  cnvepimaex  37671  dmqseq  37976  prter3  38218  atbase  38625  llnbase  38846  lplnbase  38871  lvolbase  38915  lhpbase  39335  rernegcl  41709  renegadd  41710  reneg0addlid  41712  sn-0ne2  41744  3cubes  41893  mzpsubmpt  41946  mzpnegmpt  41947  eliunov2  42895  iunrelexp0  42918  enmappwid  43216  uunT1  44006  nnfoctb  44198  rn1st  44439  afveu  46322  afv2eu  46407  afv20fv0  46432  fzopredsuc  46492  fargshiftfva  46572  lindsrng01  47313