Theorem mpancom 684

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  mpan  686  spesbc  3875  csbie2df  4439  xpiindi  5834  fununfun  6595  dffv2  6985  elunirn2OLD  7254  fliftcnv  7310  riotaprop  7395  elovmpt3rab1  7668  3xpexg  7741  orduniorsuc  7820  unielxp  8015  dmtpos  8225  tpossym  8245  wfrlem5OLD  8315  oesuclem  8527  ercnv  8726  cnvct  9036  undomOLD  9062  pwfilem  9179  sucxpdom  9257  enp1i  9281  3xpfi  9321  pwfilemOLD  9348  rankr1id  9859  cardnn  9960  alephnbtwn2  10069  alephsucdom  10076  cdainflem  10184  isfin4p1  10312  axcclem  10454  dmct  10521  mptct  10535  infxpidm  10559  fpwwe2lem8  10635  gchpwdom  10667  elwina  10683  elina  10684  rankcf  10774  ltexprlem4  11036  lem1  12061  ltdivp1i  12144  rpnnen1lem5  12969  eluzfz1  13512  fzpred  13553  uznfz  13588  fz0fzdiffz0  13614  fzctr  13617  flid  13777  modid0  13866  2txmodxeq0  13900  faclbnd3  14256  faclbnd4lem4  14260  bcn1  14277  hashfac  14423  repswsymballbi  14734  wrdlen2i  14897  dfrtrclrec2  15009  rtrclreclem3  15011  rtrclreclem4  15012  relexpindlem  15014  sqrtsq  15220  absrdbnd  15292  sqreulem  15310  sqreu  15311  bpoly2  16005  bpoly3  16006  gcd0id  16464  lcmgcdlem  16547  lcmftp  16577  dvdsnprmd  16631  2mulprm  16634  pcprod  16832  fldivp1  16834  invsym2  17714  pleval2i  18293  smndlsmidm  19565  subrgsubm  20475  resrhm2b  20492  cncrng  21166  pzriprnglem11  21260  znchr  21337  psrbagfsupp  21692  mattposvs  22177  smadiadetglem2  22394  tg1  22687  cldval  22747  cldss  22753  cldopn  22755  1stcrestlem  23176  refbas  23234  refssex  23235  regr1  23474  kqreg  23475  kqnrm  23476  ufilen  23654  efmndtmd  23825  symgtgp  23830  psmetdmdm  24031  icoopnst  24683  cnheiborlem  24700  cfilfcls  25022  eflogeq  26346  logdivlt  26365  logdifbnd  26734  harmonicbnd4  26751  basellem5  26825  bposlem7  27029  zabsle1  27035  addsqn2reu  27180  chto1ub  27215  chpo1ub  27219  vmadivsum  27221  dchrmusum2  27233  dchrvmasum2if  27236  dchrvmasumlema  27239  dchrvmasumiflem2  27241  dchrisum0re  27252  dchrvmasumlem  27262  rplogsum  27266  mulogsumlem  27270  logdivsum  27272  selberg2lem  27289  pntrmax  27303  pntlem3  27348  pntleml  27350  pnt2  27352  noextendlt  27408  usgredg2vlem2  28750  vtxdgelxnn0  28996  wlkonprop  29182  wksonproplem  29228  wksonproplemOLD  29229  wwlknbp  29363  wspthnp  29371  wlklnwwlkln1  29389  clwwlkf  29567  erclwwlknsym  29590  erclwwlkntr  29591  eupth0  29734  numclwwlk1lem2fo  29878  numclwlk2lem2f  29897  numclwwlk5lem  29907  hilablo  30680  hhssabloilem  30781  mayete3i  31248  homullid  31320  adjeu  31409  lnopeqi  31528  cnlnadjlem7  31593  adjbdlnb  31604  nmopcoadji  31621  bracnlnval  31634  mptctf  32209  xraddge02  32236  xrge0npcan  32462  gsumle  32512  gsumvsca1  32641  gsumvsca2  32642  baselsiga  33411  sigasspw  33412  ddeval1  33530  ddeval0  33531  braew  33538  derangen2  34463  subfaclim  34477  snmlff  34618  elfzm12  34958  gg-cncrng  35486  fnetr  35539  wl-sbal1  36731  poimirlem13  36804  poimirlem14  36805  poimirlem31  36822  poimirlem32  36823  ismblfin  36832  itg2addnclem2  36843  areacirclem2  36880  areacirc  36884  ismgmOLD  37021  ismndo2  37045  rngomndo  37106  cnvepimaex  37508  dmqseq  37813  prter3  38055  atbase  38462  llnbase  38683  lplnbase  38708  lvolbase  38752  lhpbase  39172  rernegcl  41546  renegadd  41547  reneg0addlid  41549  sn-0ne2  41581  3cubes  41730  mzpsubmpt  41783  mzpnegmpt  41784  eliunov2  42732  iunrelexp0  42755  enmappwid  43053  uunT1  43843  nnfoctb  44035  rn1st  44276  afveu  46159  afv2eu  46244  afv20fv0  46269  fzopredsuc  46329  fargshiftfva  46409  lindsrng01  47236