Theorem mpancom 700

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  mpan  702  spesbc  3836  csbie2df  4409  xpiindi  5823  fununfun  6586  dffv2  6978  fliftcnv  7311  riotaprop  7396  elovmpt3rab1  7672  3xpexg  7752  orduniorsuc  7827  unielxp  8025  dmtpos  8235  tpossym  8255  oesuclem  8511  ercnv  8717  cnvct  9032  sucxpdom  9222  enp1i  9240  pwfilem  9278  3xpfi  9281  rankr1id  9835  cardnn  9950  alephnbtwn2  10057  alephsucdom  10064  cdainflem  10172  isfin4p1  10300  axcclem  10442  dmct  10509  mptct  10523  infxpidm  10547  fpwwe2lem8  10624  gchpwdom  10656  elwina  10672  elina  10673  rankcf  10763  ltexprlem4  11025  lem1  12059  ltdivp1i  12142  nn0le2x  12559  rpnnen1lem5  13006  eluzfz1  13560  fzpred  13602  uznfz  13640  fz0fzdiffz0  13667  fzctr  13670  flid  13843  modid0  13932  2txmodxeq0  13969  faclbnd3  14330  faclbnd4lem4  14334  bcn1  14351  hashfac  14497  repswsymballbi  14819  wrdlen2i  14981  dfrtrclrec2  15097  rtrclreclem3  15099  rtrclreclem4  15100  relexpindlem  15102  sqrtsq  15322  absrdbnd  15395  sqreulem  15413  sqreu  15414  bpoly2  16112  bpoly3  16113  gcd0id  16578  lcmgcdlem  16665  lcmftp  16695  dvdsnprmd  16749  2mulprm  16752  pcprod  16956  fldivp1  16958  invsym2  17821  pleval2i  18391  smndlsmidm  19727  gsumle  20216  subrgsubm  20671  resrhm2b  20688  pzriprnglem11  21622  znchr  21693  psrbagfsupp  22050  mattposvs  22593  smadiadetglem2  22810  tg1  23102  cldval  23161  cldss  23167  cldopn  23169  1stcrestlem  23590  refbas  23648  refssex  23649  regr1  23888  kqreg  23889  kqnrm  23890  ufilen  24068  efmndtmd  24239  symgtgp  24244  psmetdmdm  24443  icoopnst  25079  cnheiborlem  25094  cfilfcls  25414  eflogeq  26748  logdivlt  26767  logdifbnd  27139  harmonicbnd4  27156  basellem5  27230  bposlem7  27435  zabsle1  27441  addsqn2reu  27586  chto1ub  27621  chpo1ub  27625  vmadivsum  27627  dchrmusum2  27639  dchrvmasum2if  27642  dchrvmasumlema  27645  dchrvmasumiflem2  27647  dchrisum0re  27658  dchrvmasumlem  27668  rplogsum  27672  mulogsumlem  27676  logdivsum  27678  selberg2lem  27695  pntrmax  27709  pntlem3  27754  pntleml  27756  pnt2  27758  noextendlt  27814  usgredg2vlem2  29557  vtxdgelxnn0  29803  wlkonprop  29987  wksonproplem  30033  wwlknbp  30172  wspthnp  30180  wlklnwwlkln1  30198  clwwlkf  30379  erclwwlknsym  30402  erclwwlkntr  30403  eupth0  30546  numclwwlk1lem2fo  30690  numclwlk2lem2f  30709  numclwwlk5lem  30719  hilablo  31493  hhssabloilem  31594  mayete3i  32061  homullid  32133  adjeu  32222  lnopeqi  32341  cnlnadjlem7  32406  adjbdlnb  32417  nmopcoadji  32434  bracnlnval  32447  mptctf  33042  xraddge02  33083  xrge0npcan  33321  gsumvsca1  33527  gsumvsca2  33528  baselsiga  34486  sigasspw  34487  ddeval1  34605  ddeval0  34606  braew  34613  derangen2  35647  subfaclim  35661  snmlff  35802  elfzm12  36148  fnetr  36843  wl-sbal1  38199  poimirlem13  38265  poimirlem14  38266  poimirlem31  38283  poimirlem32  38284  ismblfin  38293  itg2addnclem2  38304  areacirclem2  38341  areacirc  38345  ismgmOLD  38482  ismndo2  38506  rngomndo  38567  ecxrn2  39038  dmqseq  39354  prter3  39637  atbase  40044  llnbase  40264  lplnbase  40289  lvolbase  40333  lhpbase  40753  rernegcl  43113  renegadd  43114  reneg0addlid  43116  sn-0ne2  43148  3cubes  43404  mzpsubmpt  43457  mzpnegmpt  43458  eliunov2  44388  iunrelexp0  44411  enmappwid  44709  uunT1  45471  nnfoctb  45751  rn1st  45971  afveu  47873  afv2eu  47958  afv20fv0  47983  fzopredsuc  48044  fargshiftfva  48175  lindsrng01  49231  cic1st2nd  49808  cicpropdlem  49810  zeroo2  49995