Theorem mpancom 698

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpan  700  spesbc  3833  csbie2df  4394  xpiindi  5803  fununfun  6563  dffv2  6956  fliftcnv  7289  riotaprop  7374  elovmpt3rab1  7650  3xpexg  7729  orduniorsuc  7804  unielxp  8002  dmtpos  8211  tpossym  8231  oesuclem  8487  ercnv  8693  cnvct  9008  sucxpdom  9198  enp1i  9216  pwfilem  9255  3xpfi  9258  rankr1id  9813  cardnn  9914  alephnbtwn2  10021  alephsucdom  10028  cdainflem  10137  isfin4p1  10265  axcclem  10407  dmct  10474  mptct  10488  infxpidm  10512  fpwwe2lem8  10589  gchpwdom  10621  elwina  10637  elina  10638  rankcf  10728  ltexprlem4  10990  lem1  12027  ltdivp1i  12111  nn0le2x  12528  rpnnen1lem5  12975  eluzfz1  13529  fzpred  13570  uznfz  13608  fz0fzdiffz0  13635  fzctr  13638  flid  13811  modid0  13900  2txmodxeq0  13937  faclbnd3  14298  faclbnd4lem4  14302  bcn1  14319  hashfac  14464  repswsymballbi  14786  wrdlen2i  14948  dfrtrclrec2  15064  rtrclreclem3  15066  rtrclreclem4  15067  relexpindlem  15069  sqrtsq  15286  absrdbnd  15359  sqreulem  15377  sqreu  15378  bpoly2  16077  bpoly3  16078  gcd0id  16543  lcmgcdlem  16630  lcmftp  16660  dvdsnprmd  16714  2mulprm  16717  pcprod  16921  fldivp1  16923  invsym2  17786  pleval2i  18356  smndlsmidm  19686  gsumle  20175  subrgsubm  20621  resrhm2b  20638  pzriprnglem11  21530  znchr  21601  psrbagfsupp  21958  mattposvs  22502  smadiadetglem2  22719  tg1  23011  cldval  23070  cldss  23076  cldopn  23078  1stcrestlem  23499  refbas  23557  refssex  23558  regr1  23797  kqreg  23798  kqnrm  23799  ufilen  23977  efmndtmd  24148  symgtgp  24153  psmetdmdm  24352  icoopnst  24988  cnheiborlem  25003  cfilfcls  25323  eflogeq  26654  logdivlt  26673  logdifbnd  27045  harmonicbnd4  27062  basellem5  27136  bposlem7  27341  zabsle1  27347  addsqn2reu  27492  chto1ub  27527  chpo1ub  27531  vmadivsum  27533  dchrmusum2  27545  dchrvmasum2if  27548  dchrvmasumlema  27551  dchrvmasumiflem2  27553  dchrisum0re  27564  dchrvmasumlem  27574  rplogsum  27578  mulogsumlem  27582  logdivsum  27584  selberg2lem  27601  pntrmax  27615  pntlem3  27660  pntleml  27662  pnt2  27664  noextendlt  27720  usgredg2vlem2  29383  vtxdgelxnn0  29629  wlkonprop  29813  wksonproplem  29859  wwlknbp  29998  wspthnp  30006  wlklnwwlkln1  30024  clwwlkf  30205  erclwwlknsym  30228  erclwwlkntr  30229  eupth0  30372  numclwwlk1lem2fo  30516  numclwlk2lem2f  30535  numclwwlk5lem  30545  hilablo  31319  hhssabloilem  31420  mayete3i  31887  homullid  31959  adjeu  32048  lnopeqi  32167  cnlnadjlem7  32232  adjbdlnb  32243  nmopcoadji  32260  bracnlnval  32273  mptctf  32878  xraddge02  32919  xrge0npcan  33158  gsumvsca1  33366  gsumvsca2  33367  baselsiga  34372  sigasspw  34373  ddeval1  34491  ddeval0  34492  braew  34499  derangen2  35484  subfaclim  35498  snmlff  35639  elfzm12  35985  fnetr  36671  wl-sbal1  38026  poimirlem13  38092  poimirlem14  38093  poimirlem31  38110  poimirlem32  38111  ismblfin  38120  itg2addnclem2  38131  areacirclem2  38168  areacirc  38172  ismgmOLD  38309  ismndo2  38333  rngomndo  38394  ecxrn2  38867  dmqseq  39183  prter3  39466  atbase  39873  llnbase  40093  lplnbase  40118  lvolbase  40162  lhpbase  40582  rernegcl  42940  renegadd  42941  reneg0addlid  42943  sn-0ne2  42975  3cubes  43231  mzpsubmpt  43284  mzpnegmpt  43285  eliunov2  44215  iunrelexp0  44238  enmappwid  44536  uunT1  45315  nnfoctb  45588  rn1st  45808  afveu  47707  afv2eu  47792  afv20fv0  47817  fzopredsuc  47878  fargshiftfva  48009  lindsrng01  49050  cic1st2nd  49628  cicpropdlem  49630  zeroo2  49815