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  3811  csbie2df  4348  xpiindi  5670  fununfun  6372  dffv2  6733  fliftcnv  7043  riotaprop  7120  elovmpt3rab1  7385  3xpexg  7455  orduniorsuc  7525  unielxp  7709  dmtpos  7887  tpossym  7907  wfrlem5  7942  oesuclem  8133  ercnv  8293  cnvct  8569  undom  8588  sucxpdom  8711  3xpfi  8774  pwfilem  8802  rankr1id  9275  cardnn  9376  alephnbtwn2  9483  alephsucdom  9490  cdainflem  9598  isfin4p1  9726  axcclem  9868  dmct  9935  mptct  9949  infxpidm  9973  fpwwe2lem9  10049  gchpwdom  10081  elwina  10097  elina  10098  rankcf  10188  ltexprlem4  10450  lem1  11472  ltdivp1i  11555  rpnnen1lem5  12368  eluzfz1  12909  fzpred  12950  uznfz  12985  fz0fzdiffz0  13011  fzctr  13014  flid  13173  modid0  13260  2txmodxeq0  13294  faclbnd3  13648  faclbnd4lem4  13652  bcn1  13669  hashfac  13812  repswsymballbi  14133  wrdlen2i  14295  dfrtrclrec2  14409  rtrclreclem3  14411  rtrclreclem4  14412  relexpindlem  14414  sqrtsq  14621  absrdbnd  14693  sqreulem  14711  sqreu  14712  bpoly2  15403  bpoly3  15404  gcd0id  15857  lcmgcdlem  15940  lcmftp  15970  dvdsnprmd  16024  2mulprm  16027  pcprod  16221  fldivp1  16223  invsym2  17025  pleval2i  17566  smndlsmidm  18773  subrgsubm  19541  cncrng  20112  znchr  20254  mattposvs  21060  smadiadetglem2  21277  tg1  21569  cldval  21628  cldss  21634  cldopn  21636  1stcrestlem  22057  refbas  22115  refssex  22116  regr1  22355  kqreg  22356  kqnrm  22357  ufilen  22535  efmndtmd  22706  symgtgp  22711  elrnust  22830  psmetdmdm  22912  metuval  23156  icoopnst  23544  cnheiborlem  23559  cfilfcls  23878  eflogeq  25193  logdivlt  25212  logdifbnd  25579  harmonicbnd4  25596  basellem5  25670  bposlem7  25874  zabsle1  25880  addsqn2reu  26025  chto1ub  26060  chpo1ub  26064  vmadivsum  26066  dchrmusum2  26078  dchrvmasum2if  26081  dchrvmasumlema  26084  dchrvmasumiflem2  26086  dchrisum0re  26097  dchrvmasumlem  26107  rplogsum  26111  mulogsumlem  26115  logdivsum  26117  selberg2lem  26134  pntrmax  26148  pntlem3  26193  pntleml  26195  pnt2  26197  usgredg2vlem2  27016  vtxdgelxnn0  27262  wlkonprop  27448  wksonproplem  27494  wwlknbp  27628  wspthnp  27636  wlklnwwlkln1  27654  clwwlkf  27832  erclwwlknsym  27855  erclwwlkntr  27856  eupth0  27999  numclwwlk1lem2fo  28143  numclwlk2lem2f  28162  numclwwlk5lem  28172  hilablo  28943  hhssabloilem  29044  mayete3i  29511  homulid2  29583  adjeu  29672  lnopeqi  29791  cnlnadjlem7  29856  adjbdlnb  29867  nmopcoadji  29884  bracnlnval  29897  elunirn2  30414  mptctf  30479  xraddge02  30506  xrge0npcan  30728  gsumle  30775  gsumvsca1  30904  gsumvsca2  30905  metidval  31243  pstmval  31248  baselsiga  31484  sigasspw  31485  ddeval1  31603  ddeval0  31604  braew  31611  derangen2  32534  subfaclim  32548  snmlff  32689  elfzm12  33031  noextendlt  33289  fnetr  33812  wl-sbal1  34964  poimirlem13  35070  poimirlem14  35071  poimirlem31  35088  poimirlem32  35089  ismblfin  35098  itg2addnclem2  35109  areacirclem2  35146  areacirc  35150  ismgmOLD  35288  ismndo2  35312  rngomndo  35373  cnvepimaex  35753  dmqseq  36035  prter3  36178  atbase  36585  llnbase  36805  lplnbase  36830  lvolbase  36874  lhpbase  37294  rernegcl  39509  renegadd  39510  reneg0addid2  39512  sn-0ne2  39544  3cubes  39631  mzpsubmpt  39684  mzpnegmpt  39685  eliunov2  40380  iunrelexp0  40403  enmappwid  40701  uunT1  41486  nnfoctb  41681  afveu  43709  afv2eu  43794  afv20fv0  43819  fzopredsuc  43880  fargshiftfva  43960  lindsrng01  44877