Theorem mpancom 686

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 396

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 397

This theorem is referenced by:  mpan  688  spesbc  3875  csbie2df  4439  xpiindi  5833  fununfun  6593  dffv2  6983  elunirn2OLD  7248  fliftcnv  7304  riotaprop  7389  elovmpt3rab1  7662  3xpexg  7735  orduniorsuc  7814  unielxp  8009  dmtpos  8219  tpossym  8239  wfrlem5OLD  8309  oesuclem  8521  ercnv  8720  cnvct  9030  undomOLD  9056  pwfilem  9173  sucxpdom  9251  enp1i  9275  3xpfi  9315  pwfilemOLD  9342  rankr1id  9853  cardnn  9954  alephnbtwn2  10063  alephsucdom  10070  cdainflem  10178  isfin4p1  10306  axcclem  10448  dmct  10515  mptct  10529  infxpidm  10553  fpwwe2lem8  10629  gchpwdom  10661  elwina  10677  elina  10678  rankcf  10768  ltexprlem4  11030  lem1  12053  ltdivp1i  12136  rpnnen1lem5  12961  eluzfz1  13504  fzpred  13545  uznfz  13580  fz0fzdiffz0  13606  fzctr  13609  flid  13769  modid0  13858  2txmodxeq0  13892  faclbnd3  14248  faclbnd4lem4  14252  bcn1  14269  hashfac  14415  repswsymballbi  14726  wrdlen2i  14889  dfrtrclrec2  15001  rtrclreclem3  15003  rtrclreclem4  15004  relexpindlem  15006  sqrtsq  15212  absrdbnd  15284  sqreulem  15302  sqreu  15303  bpoly2  15997  bpoly3  15998  gcd0id  16456  lcmgcdlem  16539  lcmftp  16569  dvdsnprmd  16623  2mulprm  16626  pcprod  16824  fldivp1  16826  invsym2  17706  pleval2i  18285  smndlsmidm  19518  subrgsubm  20368  resrhm2b  20386  cncrng  20958  znchr  21109  psrbagfsupp  21464  mattposvs  21948  smadiadetglem2  22165  tg1  22458  cldval  22518  cldss  22524  cldopn  22526  1stcrestlem  22947  refbas  23005  refssex  23006  regr1  23245  kqreg  23246  kqnrm  23247  ufilen  23425  efmndtmd  23596  symgtgp  23601  psmetdmdm  23802  icoopnst  24446  cnheiborlem  24461  cfilfcls  24782  eflogeq  26101  logdivlt  26120  logdifbnd  26487  harmonicbnd4  26504  basellem5  26578  bposlem7  26782  zabsle1  26788  addsqn2reu  26933  chto1ub  26968  chpo1ub  26972  vmadivsum  26974  dchrmusum2  26986  dchrvmasum2if  26989  dchrvmasumlema  26992  dchrvmasumiflem2  26994  dchrisum0re  27005  dchrvmasumlem  27015  rplogsum  27019  mulogsumlem  27023  logdivsum  27025  selberg2lem  27042  pntrmax  27056  pntlem3  27101  pntleml  27103  pnt2  27105  noextendlt  27161  usgredg2vlem2  28472  vtxdgelxnn0  28718  wlkonprop  28904  wksonproplem  28950  wksonproplemOLD  28951  wwlknbp  29085  wspthnp  29093  wlklnwwlkln1  29111  clwwlkf  29289  erclwwlknsym  29312  erclwwlkntr  29313  eupth0  29456  numclwwlk1lem2fo  29600  numclwlk2lem2f  29619  numclwwlk5lem  29629  hilablo  30400  hhssabloilem  30501  mayete3i  30968  homullid  31040  adjeu  31129  lnopeqi  31248  cnlnadjlem7  31313  adjbdlnb  31324  nmopcoadji  31341  bracnlnval  31354  mptctf  31929  xraddge02  31956  xrge0npcan  32182  gsumle  32229  gsumvsca1  32358  gsumvsca2  32359  baselsiga  33101  sigasspw  33102  ddeval1  33220  ddeval0  33221  braew  33228  derangen2  34153  subfaclim  34167  snmlff  34308  elfzm12  34648  fnetr  35224  wl-sbal1  36416  poimirlem13  36489  poimirlem14  36490  poimirlem31  36507  poimirlem32  36508  ismblfin  36517  itg2addnclem2  36528  areacirclem2  36565  areacirc  36569  ismgmOLD  36706  ismndo2  36730  rngomndo  36791  cnvepimaex  37193  dmqseq  37498  prter3  37740  atbase  38147  llnbase  38368  lplnbase  38393  lvolbase  38437  lhpbase  38857  rernegcl  41240  renegadd  41241  reneg0addlid  41243  sn-0ne2  41275  3cubes  41413  mzpsubmpt  41466  mzpnegmpt  41467  eliunov2  42415  iunrelexp0  42438  enmappwid  42736  uunT1  43526  nnfoctb  43719  rn1st  43964  afveu  45847  afv2eu  45932  afv20fv0  45957  fzopredsuc  46017  fargshiftfva  46097  lindsrng01  47102