Theorem mpancom 681

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  mpan  683  spesbc  3746  xpiindi  5491  fununfun  6171  dffv2  6519  fliftcnv  6817  riotaprop  6891  elovmpt3rab1  7154  3xpexg  7223  orduniorsuc  7292  unielxp  7467  dmtpos  7630  tpossym  7650  wfrlem5  7686  oesuclem  7873  ercnv  8031  cnvct  8300  undom  8318  sucxpdom  8439  3xpfi  8502  pwfilem  8530  rankr1id  9003  cardnn  9103  alephnbtwn2  9209  alephsucdom  9216  cdainflem  9329  isfin4-3  9453  axcclem  9595  dmct  9662  mptct  9676  infxpidm  9700  fpwwe2lem9  9776  gchpwdom  9808  elwina  9824  elina  9825  rankcf  9915  ltexprlem4  10177  lem1  11195  ltdivp1i  11281  rpnnen1lem5  12104  eluzfz1  12642  fzpred  12683  uznfz  12718  fz0fzdiffz0  12744  fzctr  12747  flid  12905  modid0  12992  2txmodxeq0  13026  faclbnd3  13373  faclbnd4lem4  13377  bcn1  13394  hashfac  13532  repswsymballbi  13897  wrdlen2i  14064  dfrtrclrec2  14175  rtrclreclem3  14178  rtrclreclem4  14179  relexpindlem  14181  sqrtsq  14388  absrdbnd  14459  sqreulem  14477  sqreu  14478  bpoly2  15161  gcd0id  15614  lcmgcdlem  15693  lcmftp  15723  dvdsnprmd  15776  pcprod  15971  fldivp1  15973  invsym2  16776  pleval2i  17318  subrgsubm  19150  cncrng  20128  znchr  20271  mattposvs  20630  smadiadetglem2  20848  tg1  21140  cldval  21199  cldss  21205  cldopn  21207  1stcrestlem  21627  refbas  21685  refssex  21686  regr1  21925  kqreg  21926  kqnrm  21927  ufilen  22105  symgtgp  22276  elrnust  22399  psmetdmdm  22481  metuval  22725  icoopnst  23109  cnheiborlem  23124  cfilfcls  23443  eflogeq  24748  logdivlt  24767  logdifbnd  25134  harmonicbnd4  25151  basellem5  25225  bposlem7  25429  zabsle1  25435  chto1ub  25579  chpo1ub  25583  vmadivsum  25585  dchrmusum2  25597  dchrvmasum2if  25600  dchrvmasumlema  25603  dchrvmasumiflem2  25605  dchrisum0re  25616  dchrvmasumlem  25626  rplogsum  25630  mulogsumlem  25634  logdivsum  25636  selberg2lem  25653  pntrmax  25667  pntlem3  25712  pntleml  25714  pnt2  25716  usgredg2vlem2  26523  vtxdgelxnn0  26771  wlkonprop  26956  wksonproplem  27008  wwlknbp  27142  wspthnp  27150  wlklnwwlkln1  27168  clwwlkfOLD  27393  clwwlkf  27398  erclwwlknsym  27424  erclwwlkntr  27425  clwlksfclwwlkOLD  27439  eupth0  27591  numclwwlk1lem2fo  27750  numclwwlk1lem2foOLD  27755  numclwlk2lem2f  27781  numclwlk2lem2fOLD  27784  numclwlk2lem2fOLDOLD  27792  numclwwlk5lem  27803  hilablo  28573  hhssabloilem  28674  mayete3i  29143  homulid2  29215  adjeu  29304  lnopeqi  29423  cnlnadjlem7  29488  adjbdlnb  29499  nmopcoadji  29516  bracnlnval  29529  elunirn2  30001  mptctf  30044  xraddge02  30069  xrge0npcan  30240  gsumle  30325  gsumvsca1  30328  gsumvsca2  30329  metidval  30479  pstmval  30484  baselsiga  30724  sigasspw  30725  ddeval1  30843  ddeval0  30844  braew  30851  derangen2  31703  subfaclim  31717  snmlff  31858  elfzm12  32114  frrlem5  32324  noextendlt  32362  fnetr  32885  wl-sbal1  33891  poimirlem13  33967  poimirlem14  33968  poimirlem31  33985  poimirlem32  33986  ismblfin  33995  itg2addnclem2  34006  areacirclem2  34045  areacirc  34049  ismgmOLD  34192  ismndo2  34216  rngomndo  34277  prter3  34958  atbase  35365  llnbase  35585  lplnbase  35610  lvolbase  35654  lhpbase  36074  rernegcl  38076  renegadd  38077  reneg0addid1  38080  mzpsubmpt  38151  mzpnegmpt  38152  eliunov2  38813  iunrelexp0  38836  enmappwid  39135  uunT1  39835  nnfoctb  40031  afveu  42056  afv2eu  42141  afv20fv0  42166  fzopredsuc  42222  fargshiftfva  42268  lindsrng01  43105