Theorem mpancom 687

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 587	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 210  df-an 400

This theorem is referenced by:  mpan  689  spesbc  3788  csbie2df  4337  xpiindi  5675  fununfun  6383  dffv2  6747  fliftcnv  7058  riotaprop  7135  elovmpt3rab1  7401  3xpexg  7473  orduniorsuc  7544  unielxp  7731  dmtpos  7914  tpossym  7934  wfrlem5  7969  oesuclem  8160  ercnv  8320  cnvct  8605  undom  8626  pwfilem  8745  sucxpdom  8765  3xpfi  8823  pwfilemOLD  8851  rankr1id  9324  cardnn  9425  alephnbtwn2  9532  alephsucdom  9539  cdainflem  9647  isfin4p1  9775  axcclem  9917  dmct  9984  mptct  9998  infxpidm  10022  fpwwe2lem8  10098  gchpwdom  10130  elwina  10146  elina  10147  rankcf  10237  ltexprlem4  10499  lem1  11521  ltdivp1i  11604  rpnnen1lem5  12421  eluzfz1  12963  fzpred  13004  uznfz  13039  fz0fzdiffz0  13065  fzctr  13068  flid  13227  modid0  13314  2txmodxeq0  13348  faclbnd3  13702  faclbnd4lem4  13706  bcn1  13723  hashfac  13868  repswsymballbi  14189  wrdlen2i  14351  dfrtrclrec2  14465  rtrclreclem3  14467  rtrclreclem4  14468  relexpindlem  14470  sqrtsq  14677  absrdbnd  14749  sqreulem  14767  sqreu  14768  bpoly2  15459  bpoly3  15460  gcd0id  15918  lcmgcdlem  16002  lcmftp  16032  dvdsnprmd  16086  2mulprm  16089  pcprod  16286  fldivp1  16288  invsym2  17092  pleval2i  17640  smndlsmidm  18848  subrgsubm  19616  cncrng  20187  znchr  20330  psrbagfsupp  20682  mattposvs  21155  smadiadetglem2  21372  tg1  21664  cldval  21723  cldss  21729  cldopn  21731  1stcrestlem  22152  refbas  22210  refssex  22211  regr1  22450  kqreg  22451  kqnrm  22452  ufilen  22630  efmndtmd  22801  symgtgp  22806  elrnust  22925  psmetdmdm  23007  metuval  23251  icoopnst  23640  cnheiborlem  23655  cfilfcls  23974  eflogeq  25292  logdivlt  25311  logdifbnd  25678  harmonicbnd4  25695  basellem5  25769  bposlem7  25973  zabsle1  25979  addsqn2reu  26124  chto1ub  26159  chpo1ub  26163  vmadivsum  26165  dchrmusum2  26177  dchrvmasum2if  26180  dchrvmasumlema  26183  dchrvmasumiflem2  26185  dchrisum0re  26196  dchrvmasumlem  26206  rplogsum  26210  mulogsumlem  26214  logdivsum  26216  selberg2lem  26233  pntrmax  26247  pntlem3  26292  pntleml  26294  pnt2  26296  usgredg2vlem2  27115  vtxdgelxnn0  27361  wlkonprop  27547  wksonproplem  27593  wwlknbp  27727  wspthnp  27735  wlklnwwlkln1  27753  clwwlkf  27931  erclwwlknsym  27954  erclwwlkntr  27955  eupth0  28098  numclwwlk1lem2fo  28242  numclwlk2lem2f  28261  numclwwlk5lem  28271  hilablo  29042  hhssabloilem  29143  mayete3i  29610  homulid2  29682  adjeu  29771  lnopeqi  29890  cnlnadjlem7  29955  adjbdlnb  29966  nmopcoadji  29983  bracnlnval  29996  elunirn2  30512  mptctf  30576  xraddge02  30603  xrge0npcan  30829  gsumle  30876  gsumvsca1  31005  gsumvsca2  31006  metidval  31361  pstmval  31366  baselsiga  31602  sigasspw  31603  ddeval1  31721  ddeval0  31722  braew  31729  derangen2  32652  subfaclim  32666  snmlff  32807  elfzm12  33149  noextendlt  33437  madebdaylemlrcut  33636  fnetr  34089  wl-sbal1  35244  poimirlem13  35350  poimirlem14  35351  poimirlem31  35368  poimirlem32  35369  ismblfin  35378  itg2addnclem2  35389  areacirclem2  35426  areacirc  35430  ismgmOLD  35568  ismndo2  35592  rngomndo  35653  cnvepimaex  36033  dmqseq  36315  prter3  36458  atbase  36865  llnbase  37085  lplnbase  37110  lvolbase  37154  lhpbase  37574  rernegcl  39851  renegadd  39852  reneg0addid2  39854  sn-0ne2  39886  3cubes  40004  mzpsubmpt  40057  mzpnegmpt  40058  eliunov2  40753  iunrelexp0  40776  enmappwid  41074  uunT1  41859  nnfoctb  42054  afveu  44077  afv2eu  44162  afv20fv0  44187  fzopredsuc  44248  fargshiftfva  44328  lindsrng01  45242