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  3833  csbie2df  4393  xpiindi  5775  fununfun  6529  dffv2  6917  fliftcnv  7245  riotaprop  7330  elovmpt3rab1  7606  3xpexg  7685  orduniorsuc  7760  unielxp  7959  dmtpos  8168  tpossym  8188  oesuclem  8440  ercnv  8643  cnvct  8956  sucxpdom  9145  enp1i  9163  pwfilem  9202  3xpfi  9205  rankr1id  9755  cardnn  9856  alephnbtwn2  9963  alephsucdom  9970  cdainflem  10079  isfin4p1  10206  axcclem  10348  dmct  10415  mptct  10429  infxpidm  10453  fpwwe2lem8  10529  gchpwdom  10561  elwina  10577  elina  10578  rankcf  10668  ltexprlem4  10930  lem1  11964  ltdivp1i  12048  nn0le2x  12435  rpnnen1lem5  12879  eluzfz1  13431  fzpred  13472  uznfz  13510  fz0fzdiffz0  13537  fzctr  13540  flid  13712  modid0  13801  2txmodxeq0  13838  faclbnd3  14199  faclbnd4lem4  14203  bcn1  14220  hashfac  14365  repswsymballbi  14687  wrdlen2i  14849  dfrtrclrec2  14965  rtrclreclem3  14967  rtrclreclem4  14968  relexpindlem  14970  sqrtsq  15176  absrdbnd  15249  sqreulem  15267  sqreu  15268  bpoly2  15964  bpoly3  15965  gcd0id  16430  lcmgcdlem  16517  lcmftp  16547  dvdsnprmd  16601  2mulprm  16604  pcprod  16807  fldivp1  16809  invsym2  17670  pleval2i  18240  smndlsmidm  19569  gsumle  20058  subrgsubm  20501  resrhm2b  20518  cncrngOLD  21327  pzriprnglem11  21429  znchr  21500  psrbagfsupp  21857  mattposvs  22371  smadiadetglem2  22588  tg1  22880  cldval  22939  cldss  22945  cldopn  22947  1stcrestlem  23368  refbas  23426  refssex  23427  regr1  23666  kqreg  23667  kqnrm  23668  ufilen  23846  efmndtmd  24017  symgtgp  24022  psmetdmdm  24221  icoopnst  24864  cnheiborlem  24881  cfilfcls  25202  eflogeq  26539  logdivlt  26558  logdifbnd  26932  harmonicbnd4  26949  basellem5  27023  bposlem7  27229  zabsle1  27235  addsqn2reu  27380  chto1ub  27415  chpo1ub  27419  vmadivsum  27421  dchrmusum2  27433  dchrvmasum2if  27436  dchrvmasumlema  27439  dchrvmasumiflem2  27441  dchrisum0re  27452  dchrvmasumlem  27462  rplogsum  27466  mulogsumlem  27470  logdivsum  27472  selberg2lem  27489  pntrmax  27503  pntlem3  27548  pntleml  27550  pnt2  27552  noextendlt  27609  usgredg2vlem2  29205  vtxdgelxnn0  29452  wlkonprop  29636  wksonproplem  29682  wwlknbp  29821  wspthnp  29829  wlklnwwlkln1  29847  clwwlkf  30025  erclwwlknsym  30048  erclwwlkntr  30049  eupth0  30192  numclwwlk1lem2fo  30336  numclwlk2lem2f  30355  numclwwlk5lem  30365  hilablo  31138  hhssabloilem  31239  mayete3i  31706  homullid  31778  adjeu  31867  lnopeqi  31986  cnlnadjlem7  32051  adjbdlnb  32062  nmopcoadji  32079  bracnlnval  32092  mptctf  32697  xraddge02  32738  xrge0npcan  32999  gsumvsca1  33193  gsumvsca2  33194  baselsiga  34126  sigasspw  34127  ddeval1  34245  ddeval0  34246  braew  34253  derangen2  35216  subfaclim  35230  snmlff  35371  elfzm12  35717  fnetr  36391  wl-sbal1  37603  poimirlem13  37679  poimirlem14  37680  poimirlem31  37697  poimirlem32  37698  ismblfin  37707  itg2addnclem2  37718  areacirclem2  37755  areacirc  37759  ismgmOLD  37896  ismndo2  37920  rngomndo  37981  dmqseq  38683  prter3  38927  atbase  39334  llnbase  39554  lplnbase  39579  lvolbase  39623  lhpbase  40043  rernegcl  42410  renegadd  42411  reneg0addlid  42413  sn-0ne2  42445  3cubes  42729  mzpsubmpt  42782  mzpnegmpt  42783  eliunov2  43718  iunrelexp0  43741  enmappwid  44039  uunT1  44818  nnfoctb  45091  rn1st  45316  afveu  47190  afv2eu  47275  afv20fv0  47300  fzopredsuc  47360  fargshiftfva  47480  lindsrng01  48506  cic1st2nd  49085  cicpropdlem  49087  zeroo2  49272