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  3845  csbie2df  4406  xpiindi  5799  fununfun  6564  dffv2  6956  elunirn2OLD  7227  fliftcnv  7286  riotaprop  7371  elovmpt3rab1  7649  3xpexg  7728  orduniorsuc  7805  unielxp  8006  dmtpos  8217  tpossym  8237  oesuclem  8489  ercnv  8692  cnvct  9005  sucxpdom  9202  enp1i  9224  pwfilem  9267  3xpfi  9271  rankr1id  9815  cardnn  9916  alephnbtwn2  10025  alephsucdom  10032  cdainflem  10141  isfin4p1  10268  axcclem  10410  dmct  10477  mptct  10491  infxpidm  10515  fpwwe2lem8  10591  gchpwdom  10623  elwina  10639  elina  10640  rankcf  10730  ltexprlem4  10992  lem1  12025  ltdivp1i  12109  nn0le2x  12496  rpnnen1lem5  12940  eluzfz1  13492  fzpred  13533  uznfz  13571  fz0fzdiffz0  13598  fzctr  13601  flid  13770  modid0  13859  2txmodxeq0  13896  faclbnd3  14257  faclbnd4lem4  14261  bcn1  14278  hashfac  14423  repswsymballbi  14745  wrdlen2i  14908  dfrtrclrec2  15024  rtrclreclem3  15026  rtrclreclem4  15027  relexpindlem  15029  sqrtsq  15235  absrdbnd  15308  sqreulem  15326  sqreu  15327  bpoly2  16023  bpoly3  16024  gcd0id  16489  lcmgcdlem  16576  lcmftp  16606  dvdsnprmd  16660  2mulprm  16663  pcprod  16866  fldivp1  16868  invsym2  17725  pleval2i  18295  smndlsmidm  19586  subrgsubm  20494  resrhm2b  20511  cncrngOLD  21301  pzriprnglem11  21401  znchr  21472  psrbagfsupp  21828  mattposvs  22342  smadiadetglem2  22559  tg1  22851  cldval  22910  cldss  22916  cldopn  22918  1stcrestlem  23339  refbas  23397  refssex  23398  regr1  23637  kqreg  23638  kqnrm  23639  ufilen  23817  efmndtmd  23988  symgtgp  23993  psmetdmdm  24193  icoopnst  24836  cnheiborlem  24853  cfilfcls  25174  eflogeq  26511  logdivlt  26530  logdifbnd  26904  harmonicbnd4  26921  basellem5  26995  bposlem7  27201  zabsle1  27207  addsqn2reu  27352  chto1ub  27387  chpo1ub  27391  vmadivsum  27393  dchrmusum2  27405  dchrvmasum2if  27408  dchrvmasumlema  27411  dchrvmasumiflem2  27413  dchrisum0re  27424  dchrvmasumlem  27434  rplogsum  27438  mulogsumlem  27442  logdivsum  27444  selberg2lem  27461  pntrmax  27475  pntlem3  27520  pntleml  27522  pnt2  27524  noextendlt  27581  usgredg2vlem2  29153  vtxdgelxnn0  29400  wlkonprop  29586  wksonproplem  29632  wksonproplemOLD  29633  wwlknbp  29772  wspthnp  29780  wlklnwwlkln1  29798  clwwlkf  29976  erclwwlknsym  29999  erclwwlkntr  30000  eupth0  30143  numclwwlk1lem2fo  30287  numclwlk2lem2f  30306  numclwwlk5lem  30316  hilablo  31089  hhssabloilem  31190  mayete3i  31657  homullid  31729  adjeu  31818  lnopeqi  31937  cnlnadjlem7  32002  adjbdlnb  32013  nmopcoadji  32030  bracnlnval  32043  mptctf  32641  xraddge02  32680  xrge0npcan  32961  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  baselsiga  34105  sigasspw  34106  ddeval1  34224  ddeval0  34225  braew  34232  derangen2  35161  subfaclim  35175  snmlff  35316  elfzm12  35662  fnetr  36339  wl-sbal1  37551  poimirlem13  37627  poimirlem14  37628  poimirlem31  37645  poimirlem32  37646  ismblfin  37655  itg2addnclem2  37666  areacirclem2  37703  areacirc  37707  ismgmOLD  37844  ismndo2  37868  rngomndo  37929  dmqseq  38631  prter3  38875  atbase  39282  llnbase  39503  lplnbase  39528  lvolbase  39572  lhpbase  39992  rernegcl  42359  renegadd  42360  reneg0addlid  42362  sn-0ne2  42394  3cubes  42678  mzpsubmpt  42731  mzpnegmpt  42732  eliunov2  43668  iunrelexp0  43691  enmappwid  43989  uunT1  44769  nnfoctb  45042  rn1st  45267  afveu  47154  afv2eu  47239  afv20fv0  47264  fzopredsuc  47324  fargshiftfva  47444  lindsrng01  48457  cic1st2nd  49036  cicpropdlem  49038  zeroo2  49223