Theorem mpancom 687

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mpan  689  spesbc  3877  csbie2df  4441  xpiindi  5836  fununfun  6597  dffv2  6987  elunirn2OLD  7252  fliftcnv  7308  riotaprop  7393  elovmpt3rab1  7666  3xpexg  7739  orduniorsuc  7818  unielxp  8013  dmtpos  8223  tpossym  8243  wfrlem5OLD  8313  oesuclem  8525  ercnv  8724  cnvct  9034  undomOLD  9060  pwfilem  9177  sucxpdom  9255  enp1i  9279  3xpfi  9319  pwfilemOLD  9346  rankr1id  9857  cardnn  9958  alephnbtwn2  10067  alephsucdom  10074  cdainflem  10182  isfin4p1  10310  axcclem  10452  dmct  10519  mptct  10533  infxpidm  10557  fpwwe2lem8  10633  gchpwdom  10665  elwina  10681  elina  10682  rankcf  10772  ltexprlem4  11034  lem1  12057  ltdivp1i  12140  rpnnen1lem5  12965  eluzfz1  13508  fzpred  13549  uznfz  13584  fz0fzdiffz0  13610  fzctr  13613  flid  13773  modid0  13862  2txmodxeq0  13896  faclbnd3  14252  faclbnd4lem4  14256  bcn1  14273  hashfac  14419  repswsymballbi  14730  wrdlen2i  14893  dfrtrclrec2  15005  rtrclreclem3  15007  rtrclreclem4  15008  relexpindlem  15010  sqrtsq  15216  absrdbnd  15288  sqreulem  15306  sqreu  15307  bpoly2  16001  bpoly3  16002  gcd0id  16460  lcmgcdlem  16543  lcmftp  16573  dvdsnprmd  16627  2mulprm  16630  pcprod  16828  fldivp1  16830  invsym2  17710  pleval2i  18289  smndlsmidm  19524  subrgsubm  20332  resrhm2b  20349  cncrng  20966  znchr  21118  psrbagfsupp  21473  mattposvs  21957  smadiadetglem2  22174  tg1  22467  cldval  22527  cldss  22533  cldopn  22535  1stcrestlem  22956  refbas  23014  refssex  23015  regr1  23254  kqreg  23255  kqnrm  23256  ufilen  23434  efmndtmd  23605  symgtgp  23610  psmetdmdm  23811  icoopnst  24455  cnheiborlem  24470  cfilfcls  24791  eflogeq  26110  logdivlt  26129  logdifbnd  26498  harmonicbnd4  26515  basellem5  26589  bposlem7  26793  zabsle1  26799  addsqn2reu  26944  chto1ub  26979  chpo1ub  26983  vmadivsum  26985  dchrmusum2  26997  dchrvmasum2if  27000  dchrvmasumlema  27003  dchrvmasumiflem2  27005  dchrisum0re  27016  dchrvmasumlem  27026  rplogsum  27030  mulogsumlem  27034  logdivsum  27036  selberg2lem  27053  pntrmax  27067  pntlem3  27112  pntleml  27114  pnt2  27116  noextendlt  27172  usgredg2vlem2  28483  vtxdgelxnn0  28729  wlkonprop  28915  wksonproplem  28961  wksonproplemOLD  28962  wwlknbp  29096  wspthnp  29104  wlklnwwlkln1  29122  clwwlkf  29300  erclwwlknsym  29323  erclwwlkntr  29324  eupth0  29467  numclwwlk1lem2fo  29611  numclwlk2lem2f  29630  numclwwlk5lem  29640  hilablo  30413  hhssabloilem  30514  mayete3i  30981  homullid  31053  adjeu  31142  lnopeqi  31261  cnlnadjlem7  31326  adjbdlnb  31337  nmopcoadji  31354  bracnlnval  31367  mptctf  31942  xraddge02  31969  xrge0npcan  32195  gsumle  32242  gsumvsca1  32371  gsumvsca2  32372  baselsiga  33113  sigasspw  33114  ddeval1  33232  ddeval0  33233  braew  33240  derangen2  34165  subfaclim  34179  snmlff  34320  elfzm12  34660  fnetr  35236  wl-sbal1  36428  poimirlem13  36501  poimirlem14  36502  poimirlem31  36519  poimirlem32  36520  ismblfin  36529  itg2addnclem2  36540  areacirclem2  36577  areacirc  36581  ismgmOLD  36718  ismndo2  36742  rngomndo  36803  cnvepimaex  37205  dmqseq  37510  prter3  37752  atbase  38159  llnbase  38380  lplnbase  38405  lvolbase  38449  lhpbase  38869  rernegcl  41244  renegadd  41245  reneg0addlid  41247  sn-0ne2  41279  3cubes  41428  mzpsubmpt  41481  mzpnegmpt  41482  eliunov2  42430  iunrelexp0  42453  enmappwid  42751  uunT1  43541  nnfoctb  43734  rn1st  43978  afveu  45861  afv2eu  45946  afv20fv0  45971  fzopredsuc  46031  fargshiftfva  46111  pzriprnglem11  46815  lindsrng01  47149