Theorem mpancom 688

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 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  690  spesbc  3832  csbie2df  4395  xpiindi  5784  fununfun  6540  dffv2  6929  fliftcnv  7257  riotaprop  7342  elovmpt3rab1  7618  3xpexg  7697  orduniorsuc  7772  unielxp  7971  dmtpos  8180  tpossym  8200  oesuclem  8452  ercnv  8656  cnvct  8971  sucxpdom  9161  enp1i  9179  pwfilem  9218  3xpfi  9221  rankr1id  9774  cardnn  9875  alephnbtwn2  9982  alephsucdom  9989  cdainflem  10098  isfin4p1  10225  axcclem  10367  dmct  10434  mptct  10448  infxpidm  10472  fpwwe2lem8  10549  gchpwdom  10581  elwina  10597  elina  10598  rankcf  10688  ltexprlem4  10950  lem1  11984  ltdivp1i  12068  nn0le2x  12455  rpnnen1lem5  12894  eluzfz1  13447  fzpred  13488  uznfz  13526  fz0fzdiffz0  13553  fzctr  13556  flid  13728  modid0  13817  2txmodxeq0  13854  faclbnd3  14215  faclbnd4lem4  14219  bcn1  14236  hashfac  14381  repswsymballbi  14703  wrdlen2i  14865  dfrtrclrec2  14981  rtrclreclem3  14983  rtrclreclem4  14984  relexpindlem  14986  sqrtsq  15192  absrdbnd  15265  sqreulem  15283  sqreu  15284  bpoly2  15980  bpoly3  15981  gcd0id  16446  lcmgcdlem  16533  lcmftp  16563  dvdsnprmd  16617  2mulprm  16620  pcprod  16823  fldivp1  16825  invsym2  17687  pleval2i  18257  smndlsmidm  19585  gsumle  20074  subrgsubm  20518  resrhm2b  20535  cncrngOLD  21344  pzriprnglem11  21446  znchr  21517  psrbagfsupp  21875  mattposvs  22399  smadiadetglem2  22616  tg1  22908  cldval  22967  cldss  22973  cldopn  22975  1stcrestlem  23396  refbas  23454  refssex  23455  regr1  23694  kqreg  23695  kqnrm  23696  ufilen  23874  efmndtmd  24045  symgtgp  24050  psmetdmdm  24249  icoopnst  24892  cnheiborlem  24909  cfilfcls  25230  eflogeq  26567  logdivlt  26586  logdifbnd  26960  harmonicbnd4  26977  basellem5  27051  bposlem7  27257  zabsle1  27263  addsqn2reu  27408  chto1ub  27443  chpo1ub  27447  vmadivsum  27449  dchrmusum2  27461  dchrvmasum2if  27464  dchrvmasumlema  27467  dchrvmasumiflem2  27469  dchrisum0re  27480  dchrvmasumlem  27490  rplogsum  27494  mulogsumlem  27498  logdivsum  27500  selberg2lem  27517  pntrmax  27531  pntlem3  27576  pntleml  27578  pnt2  27580  noextendlt  27637  usgredg2vlem2  29299  vtxdgelxnn0  29546  wlkonprop  29730  wksonproplem  29776  wwlknbp  29915  wspthnp  29923  wlklnwwlkln1  29941  clwwlkf  30122  erclwwlknsym  30145  erclwwlkntr  30146  eupth0  30289  numclwwlk1lem2fo  30433  numclwlk2lem2f  30452  numclwwlk5lem  30462  hilablo  31235  hhssabloilem  31336  mayete3i  31803  homullid  31875  adjeu  31964  lnopeqi  32083  cnlnadjlem7  32148  adjbdlnb  32159  nmopcoadji  32176  bracnlnval  32189  mptctf  32795  xraddge02  32837  xrge0npcan  33102  gsumvsca1  33308  gsumvsca2  33309  baselsiga  34272  sigasspw  34273  ddeval1  34391  ddeval0  34392  braew  34399  derangen2  35368  subfaclim  35382  snmlff  35523  elfzm12  35869  fnetr  36545  wl-sbal1  37768  poimirlem13  37834  poimirlem14  37835  poimirlem31  37852  poimirlem32  37853  ismblfin  37862  itg2addnclem2  37873  areacirclem2  37910  areacirc  37914  ismgmOLD  38051  ismndo2  38075  rngomndo  38136  ecxrn2  38593  dmqseq  38898  prter3  39142  atbase  39549  llnbase  39769  lplnbase  39794  lvolbase  39838  lhpbase  40258  rernegcl  42626  renegadd  42627  reneg0addlid  42629  sn-0ne2  42661  3cubes  42932  mzpsubmpt  42985  mzpnegmpt  42986  eliunov2  43920  iunrelexp0  43943  enmappwid  44241  uunT1  45020  nnfoctb  45293  rn1st  45517  afveu  47399  afv2eu  47484  afv20fv0  47509  fzopredsuc  47569  fargshiftfva  47689  lindsrng01  48714  cic1st2nd  49292  cicpropdlem  49294  zeroo2  49479