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 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  686  spesbc  3811  csbie2df  4371  xpiindi  5733  fununfun  6466  dffv2  6845  fliftcnv  7162  riotaprop  7240  elovmpt3rab1  7507  3xpexg  7580  orduniorsuc  7652  unielxp  7842  dmtpos  8025  tpossym  8045  wfrlem5OLD  8115  oesuclem  8317  ercnv  8477  cnvct  8778  undom  8800  pwfilem  8922  sucxpdom  8961  3xpfi  9016  pwfilemOLD  9043  rankr1id  9551  cardnn  9652  alephnbtwn2  9759  alephsucdom  9766  cdainflem  9874  isfin4p1  10002  axcclem  10144  dmct  10211  mptct  10225  infxpidm  10249  fpwwe2lem8  10325  gchpwdom  10357  elwina  10373  elina  10374  rankcf  10464  ltexprlem4  10726  lem1  11748  ltdivp1i  11831  rpnnen1lem5  12650  eluzfz1  13192  fzpred  13233  uznfz  13268  fz0fzdiffz0  13294  fzctr  13297  flid  13456  modid0  13545  2txmodxeq0  13579  faclbnd3  13934  faclbnd4lem4  13938  bcn1  13955  hashfac  14100  repswsymballbi  14421  wrdlen2i  14583  dfrtrclrec2  14697  rtrclreclem3  14699  rtrclreclem4  14700  relexpindlem  14702  sqrtsq  14909  absrdbnd  14981  sqreulem  14999  sqreu  15000  bpoly2  15695  bpoly3  15696  gcd0id  16154  lcmgcdlem  16239  lcmftp  16269  dvdsnprmd  16323  2mulprm  16326  pcprod  16524  fldivp1  16526  invsym2  17392  pleval2i  17969  smndlsmidm  19176  subrgsubm  19952  cncrng  20531  znchr  20682  psrbagfsupp  21033  mattposvs  21512  smadiadetglem2  21729  tg1  22022  cldval  22082  cldss  22088  cldopn  22090  1stcrestlem  22511  refbas  22569  refssex  22570  regr1  22809  kqreg  22810  kqnrm  22811  ufilen  22989  efmndtmd  23160  symgtgp  23165  elrnust  23284  psmetdmdm  23366  metuval  23611  icoopnst  24008  cnheiborlem  24023  cfilfcls  24343  eflogeq  25662  logdivlt  25681  logdifbnd  26048  harmonicbnd4  26065  basellem5  26139  bposlem7  26343  zabsle1  26349  addsqn2reu  26494  chto1ub  26529  chpo1ub  26533  vmadivsum  26535  dchrmusum2  26547  dchrvmasum2if  26550  dchrvmasumlema  26553  dchrvmasumiflem2  26555  dchrisum0re  26566  dchrvmasumlem  26576  rplogsum  26580  mulogsumlem  26584  logdivsum  26586  selberg2lem  26603  pntrmax  26617  pntlem3  26662  pntleml  26664  pnt2  26666  usgredg2vlem2  27496  vtxdgelxnn0  27742  wlkonprop  27928  wksonproplem  27974  wwlknbp  28108  wspthnp  28116  wlklnwwlkln1  28134  clwwlkf  28312  erclwwlknsym  28335  erclwwlkntr  28336  eupth0  28479  numclwwlk1lem2fo  28623  numclwlk2lem2f  28642  numclwwlk5lem  28652  hilablo  29423  hhssabloilem  29524  mayete3i  29991  homulid2  30063  adjeu  30152  lnopeqi  30271  cnlnadjlem7  30336  adjbdlnb  30347  nmopcoadji  30364  bracnlnval  30377  elunirn2  30890  mptctf  30954  xraddge02  30981  xrge0npcan  31205  gsumle  31252  gsumvsca1  31381  gsumvsca2  31382  metidval  31742  pstmval  31747  baselsiga  31983  sigasspw  31984  ddeval1  32102  ddeval0  32103  braew  32110  derangen2  33036  subfaclim  33050  snmlff  33191  elfzm12  33533  noextendlt  33799  madebdaylemlrcut  34006  fnetr  34467  wl-sbal1  35645  poimirlem13  35717  poimirlem14  35718  poimirlem31  35735  poimirlem32  35736  ismblfin  35745  itg2addnclem2  35756  areacirclem2  35793  areacirc  35797  ismgmOLD  35935  ismndo2  35959  rngomndo  36020  cnvepimaex  36398  dmqseq  36680  prter3  36823  atbase  37230  llnbase  37450  lplnbase  37475  lvolbase  37519  lhpbase  37939  rernegcl  40275  renegadd  40276  reneg0addid2  40278  sn-0ne2  40310  3cubes  40428  mzpsubmpt  40481  mzpnegmpt  40482  eliunov2  41176  iunrelexp0  41199  enmappwid  41497  uunT1  42289  nnfoctb  42484  afveu  44532  afv2eu  44617  afv20fv0  44642  fzopredsuc  44703  fargshiftfva  44783  lindsrng01  45697