Theorem mpancom 701

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 23	. 2 ⊢ (𝜓 → 𝜓)
3		mpancom.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜓 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpan  703  spesbc  3838  csbie2df  4411  xpiindi  5826  fununfun  6591  dffv2  6983  fliftcnv  7320  riotaprop  7407  elovmpt3rab1  7683  3xpexg  7760  orduniorsuc  7835  unielxp  8033  dmtpos  8243  tpossym  8263  oesuclem  8519  ercnv  8725  cnvct  9041  sucxpdom  9231  enp1i  9249  pwfilem  9287  3xpfi  9290  rankr1id  9844  cardnn  9968  alephnbtwn2  10075  alephsucdom  10082  cdainflem  10190  isfin4p1  10317  axcclem  10459  dmct  10526  mptct  10540  infxpidm  10564  fpwwe2lem8  10641  gchpwdom  10673  elwina  10689  elina  10690  rankcf  10780  ltexprlem4  11042  lem1  12076  ltdivp1i  12159  nn0le2x  12576  rpnnen1lem5  13023  eluzfz1  13577  fzpred  13619  uznfz  13657  fz0fzdiffz0  13684  fzctr  13687  flid  13861  modid0  13950  2txmodxeq0  13987  faclbnd3  14348  faclbnd4lem4  14352  bcn1  14369  hashfac  14515  repswsymballbi  14843  wrdlen2i  15005  dfrtrclrec2  15121  rtrclreclem3  15123  rtrclreclem4  15124  relexpindlem  15126  sqrtsq  15346  absrdbnd  15419  sqreulem  15437  sqreu  15438  bpoly2  16136  bpoly3  16137  gcd0id  16602  lcmgcdlem  16689  lcmftp  16719  dvdsnprmd  16773  2mulprm  16776  pcprod  16980  fldivp1  16982  invsym2  17845  pleval2i  18415  smndlsmidm  19757  gsumle  20246  subrgsubm  20721  resrhm2b  20738  pzriprnglem11  21678  znchr  21749  psrbagfsupp  22106  mattposvs  22649  smadiadetglem2  22866  tg1  23158  cldval  23217  cldss  23223  cldopn  23225  1stcrestlem  23646  refbas  23704  refssex  23705  regr1  23944  kqreg  23945  kqnrm  23946  ufilen  24124  efmndtmd  24295  symgtgp  24300  psmetdmdm  24499  icoopnst  25135  cnheiborlem  25150  cfilfcls  25470  eflogeq  26804  logdivlt  26823  logdifbnd  27195  harmonicbnd4  27212  basellem5  27286  bposlem7  27491  zabsle1  27497  addsqn2reu  27642  chto1ub  27677  chpo1ub  27681  vmadivsum  27683  dchrmusum2  27695  dchrvmasum2if  27698  dchrvmasumlema  27701  dchrvmasumiflem2  27703  dchrisum0re  27714  dchrvmasumlem  27724  rplogsum  27728  mulogsumlem  27732  logdivsum  27734  selberg2lem  27751  pntrmax  27765  pntlem3  27810  pntleml  27812  pnt2  27814  noextendlt  27870  usgredg2vlem2  29613  vtxdgelxnn0  29859  wlkonprop  30043  wksonproplem  30089  wwlknbp  30228  wspthnp  30236  wlklnwwlkln1  30254  clwwlkf  30435  erclwwlknsym  30458  erclwwlkntr  30459  eupth0  30602  numclwwlk1lem2fo  30746  numclwlk2lem2f  30765  numclwwlk5lem  30775  hilablo  31549  hhssabloilem  31650  mayete3i  32117  homullid  32189  adjeu  32278  lnopeqi  32397  cnlnadjlem7  32462  adjbdlnb  32473  nmopcoadji  32490  bracnlnval  32503  mptctf  33098  xraddge02  33139  xrge0npcan  33371  gsumvsca1  33577  gsumvsca2  33578  baselsiga  34536  sigasspw  34537  ddeval1  34656  ddeval0  34657  braew  34664  derangen2  35687  subfaclim  35701  snmlff  35842  elfzm12  36188  fnetr  36903  wl-sbal1  38259  poimirlem13  38325  poimirlem14  38326  poimirlem31  38343  poimirlem32  38344  ismblfin  38353  itg2addnclem2  38364  areacirclem2  38401  areacirc  38405  ismgmOLD  38542  ismndo2  38566  rngomndo  38627  ecxrn2  39098  dmqseq  39414  prter3  39697  atbase  40104  llnbase  40324  lplnbase  40349  lvolbase  40393  lhpbase  40813  rernegcl  43173  renegadd  43174  reneg0addlid  43176  sn-0ne2  43208  3cubes  43462  mzpsubmpt  43515  mzpnegmpt  43516  eliunov2  44446  iunrelexp0  44469  enmappwid  44767  uunT1  45529  nnfoctb  45809  rn1st  46029  afveu  47931  afv2eu  48016  afv20fv0  48041  fzopredsuc  48102  fargshiftfva  48233  lindsrng01  49289  cic1st2nd  49866  cicpropdlem  49868  zeroo2  50053