Theorem mpancom 689

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 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  691  spesbc  3820  csbie2df  4383  xpiindi  5790  fununfun  6546  dffv2  6935  fliftcnv  7266  riotaprop  7351  elovmpt3rab1  7627  3xpexg  7706  orduniorsuc  7781  unielxp  7980  dmtpos  8188  tpossym  8208  oesuclem  8460  ercnv  8665  cnvct  8981  sucxpdom  9171  enp1i  9189  pwfilem  9228  3xpfi  9231  rankr1id  9786  cardnn  9887  alephnbtwn2  9994  alephsucdom  10001  cdainflem  10110  isfin4p1  10237  axcclem  10379  dmct  10446  mptct  10460  infxpidm  10484  fpwwe2lem8  10561  gchpwdom  10593  elwina  10609  elina  10610  rankcf  10700  ltexprlem4  10962  lem1  11998  ltdivp1i  12082  nn0le2x  12491  rpnnen1lem5  12931  eluzfz1  13485  fzpred  13526  uznfz  13564  fz0fzdiffz0  13591  fzctr  13594  flid  13767  modid0  13856  2txmodxeq0  13893  faclbnd3  14254  faclbnd4lem4  14258  bcn1  14275  hashfac  14420  repswsymballbi  14742  wrdlen2i  14904  dfrtrclrec2  15020  rtrclreclem3  15022  rtrclreclem4  15023  relexpindlem  15025  sqrtsq  15231  absrdbnd  15304  sqreulem  15322  sqreu  15323  bpoly2  16022  bpoly3  16023  gcd0id  16488  lcmgcdlem  16575  lcmftp  16605  dvdsnprmd  16659  2mulprm  16662  pcprod  16866  fldivp1  16868  invsym2  17730  pleval2i  18300  smndlsmidm  19631  gsumle  20120  subrgsubm  20562  resrhm2b  20579  pzriprnglem11  21471  znchr  21542  psrbagfsupp  21899  mattposvs  22420  smadiadetglem2  22637  tg1  22929  cldval  22988  cldss  22994  cldopn  22996  1stcrestlem  23417  refbas  23475  refssex  23476  regr1  23715  kqreg  23716  kqnrm  23717  ufilen  23895  efmndtmd  24066  symgtgp  24071  psmetdmdm  24270  icoopnst  24906  cnheiborlem  24921  cfilfcls  25241  eflogeq  26566  logdivlt  26585  logdifbnd  26957  harmonicbnd4  26974  basellem5  27048  bposlem7  27253  zabsle1  27259  addsqn2reu  27404  chto1ub  27439  chpo1ub  27443  vmadivsum  27445  dchrmusum2  27457  dchrvmasum2if  27460  dchrvmasumlema  27463  dchrvmasumiflem2  27465  dchrisum0re  27476  dchrvmasumlem  27486  rplogsum  27490  mulogsumlem  27494  logdivsum  27496  selberg2lem  27513  pntrmax  27527  pntlem3  27572  pntleml  27574  pnt2  27576  noextendlt  27633  usgredg2vlem2  29295  vtxdgelxnn0  29541  wlkonprop  29725  wksonproplem  29771  wwlknbp  29910  wspthnp  29918  wlklnwwlkln1  29936  clwwlkf  30117  erclwwlknsym  30140  erclwwlkntr  30141  eupth0  30284  numclwwlk1lem2fo  30428  numclwlk2lem2f  30447  numclwwlk5lem  30457  hilablo  31231  hhssabloilem  31332  mayete3i  31799  homullid  31871  adjeu  31960  lnopeqi  32079  cnlnadjlem7  32144  adjbdlnb  32155  nmopcoadji  32172  bracnlnval  32185  mptctf  32789  xraddge02  32830  xrge0npcan  33080  gsumvsca1  33287  gsumvsca2  33288  baselsiga  34259  sigasspw  34260  ddeval1  34378  ddeval0  34379  braew  34386  derangen2  35356  subfaclim  35370  snmlff  35511  elfzm12  35857  fnetr  36533  wl-sbal1  37888  poimirlem13  37954  poimirlem14  37955  poimirlem31  37972  poimirlem32  37973  ismblfin  37982  itg2addnclem2  37993  areacirclem2  38030  areacirc  38034  ismgmOLD  38171  ismndo2  38195  rngomndo  38256  ecxrn2  38729  dmqseq  39045  prter3  39328  atbase  39735  llnbase  39955  lplnbase  39980  lvolbase  40024  lhpbase  40444  rernegcl  42803  renegadd  42804  reneg0addlid  42806  sn-0ne2  42838  3cubes  43122  mzpsubmpt  43175  mzpnegmpt  43176  eliunov2  44106  iunrelexp0  44129  enmappwid  44427  uunT1  45206  nnfoctb  45479  rn1st  45702  afveu  47601  afv2eu  47686  afv20fv0  47711  fzopredsuc  47772  fargshiftfva  47903  lindsrng01  48944  cic1st2nd  49522  cicpropdlem  49524  zeroo2  49709