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  3821  csbie2df  4384  xpiindi  5784  fununfun  6540  dffv2  6929  fliftcnv  7259  riotaprop  7344  elovmpt3rab1  7620  3xpexg  7699  orduniorsuc  7774  unielxp  7973  dmtpos  8181  tpossym  8201  oesuclem  8453  ercnv  8658  cnvct  8974  sucxpdom  9164  enp1i  9182  pwfilem  9221  3xpfi  9224  rankr1id  9777  cardnn  9878  alephnbtwn2  9985  alephsucdom  9992  cdainflem  10101  isfin4p1  10228  axcclem  10370  dmct  10437  mptct  10451  infxpidm  10475  fpwwe2lem8  10552  gchpwdom  10584  elwina  10600  elina  10601  rankcf  10691  ltexprlem4  10953  lem1  11989  ltdivp1i  12073  nn0le2x  12482  rpnnen1lem5  12922  eluzfz1  13476  fzpred  13517  uznfz  13555  fz0fzdiffz0  13582  fzctr  13585  flid  13758  modid0  13847  2txmodxeq0  13884  faclbnd3  14245  faclbnd4lem4  14249  bcn1  14266  hashfac  14411  repswsymballbi  14733  wrdlen2i  14895  dfrtrclrec2  15011  rtrclreclem3  15013  rtrclreclem4  15014  relexpindlem  15016  sqrtsq  15222  absrdbnd  15295  sqreulem  15313  sqreu  15314  bpoly2  16013  bpoly3  16014  gcd0id  16479  lcmgcdlem  16566  lcmftp  16596  dvdsnprmd  16650  2mulprm  16653  pcprod  16857  fldivp1  16859  invsym2  17721  pleval2i  18291  smndlsmidm  19622  gsumle  20111  subrgsubm  20553  resrhm2b  20570  cncrngOLD  21379  pzriprnglem11  21481  znchr  21552  psrbagfsupp  21909  mattposvs  22430  smadiadetglem2  22647  tg1  22939  cldval  22998  cldss  23004  cldopn  23006  1stcrestlem  23427  refbas  23485  refssex  23486  regr1  23725  kqreg  23726  kqnrm  23727  ufilen  23905  efmndtmd  24076  symgtgp  24081  psmetdmdm  24280  icoopnst  24916  cnheiborlem  24931  cfilfcls  25251  eflogeq  26579  logdivlt  26598  logdifbnd  26971  harmonicbnd4  26988  basellem5  27062  bposlem7  27267  zabsle1  27273  addsqn2reu  27418  chto1ub  27453  chpo1ub  27457  vmadivsum  27459  dchrmusum2  27471  dchrvmasum2if  27474  dchrvmasumlema  27477  dchrvmasumiflem2  27479  dchrisum0re  27490  dchrvmasumlem  27500  rplogsum  27504  mulogsumlem  27508  logdivsum  27510  selberg2lem  27527  pntrmax  27541  pntlem3  27586  pntleml  27588  pnt2  27590  noextendlt  27647  usgredg2vlem2  29309  vtxdgelxnn0  29556  wlkonprop  29740  wksonproplem  29786  wwlknbp  29925  wspthnp  29933  wlklnwwlkln1  29951  clwwlkf  30132  erclwwlknsym  30155  erclwwlkntr  30156  eupth0  30299  numclwwlk1lem2fo  30443  numclwlk2lem2f  30462  numclwwlk5lem  30472  hilablo  31246  hhssabloilem  31347  mayete3i  31814  homullid  31886  adjeu  31975  lnopeqi  32094  cnlnadjlem7  32159  adjbdlnb  32170  nmopcoadji  32187  bracnlnval  32200  mptctf  32804  xraddge02  32845  xrge0npcan  33095  gsumvsca1  33302  gsumvsca2  33303  baselsiga  34275  sigasspw  34276  ddeval1  34394  ddeval0  34395  braew  34402  derangen2  35372  subfaclim  35386  snmlff  35527  elfzm12  35873  fnetr  36549  wl-sbal1  37902  poimirlem13  37968  poimirlem14  37969  poimirlem31  37986  poimirlem32  37987  ismblfin  37996  itg2addnclem2  38007  areacirclem2  38044  areacirc  38048  ismgmOLD  38185  ismndo2  38209  rngomndo  38270  ecxrn2  38743  dmqseq  39059  prter3  39342  atbase  39749  llnbase  39969  lplnbase  39994  lvolbase  40038  lhpbase  40458  rernegcl  42817  renegadd  42818  reneg0addlid  42820  sn-0ne2  42852  3cubes  43136  mzpsubmpt  43189  mzpnegmpt  43190  eliunov2  44124  iunrelexp0  44147  enmappwid  44445  uunT1  45224  nnfoctb  45497  rn1st  45720  afveu  47613  afv2eu  47698  afv20fv0  47723  fzopredsuc  47784  fargshiftfva  47915  lindsrng01  48956  cic1st2nd  49534  cicpropdlem  49536  zeroo2  49721