Theorem mpcom 38

Description: Modus ponens inference with commutation of antecedents. Commuted form of mpd 15. (Contributed by NM, 17-Mar-1996.)

Hypotheses

Ref	Expression
mpcom.1	⊢ (𝜓 → 𝜑)
mpcom.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpcom	⊢ (𝜓 → 𝜒)

Proof of Theorem mpcom

Step	Hyp	Ref	Expression
1		mpcom.1	. 2 ⊢ (𝜓 → 𝜑)
2		mpcom.2	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 32	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  anabsi5  669  axc16i  2435  mo4  2560  sbcn1  3809  sbcim1  3810  sbcbi1  3814  sbcel21v  3824  sbccomlem  3835  csbie2df  4409  elimasni  6065  sotri  6103  unixpid  6260  f0rn0  6748  f1ocnv  6815  funbrfv  6912  elfvmptrab1w  6998  f1dom3el3dif  7247  oprabidw  7421  oprabid  7422  oprabv  7452  ndmovordi  7583  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  elovmpt3rab1  7652  limomss  7850  unielxp  8009  bropfvvvvlem  8073  f1o2ndf1  8104  smogt  8339  tfrlem1  8347  oawordeulem  8521  omass  8547  ecopovtrn  8796  mapfvd  8855  findcard2d  9136  ssfi  9143  f1domfi  9151  php  9177  unxpdom  9207  findcard3  9236  findcard3OLD  9237  isfinite2  9252  fsuppimp  9326  fsuppunfi  9346  fsuppunbi  9347  fsuppres  9351  infsupprpr  9464  cantnfval2  9629  cantnfle  9631  cantnfp1lem3  9640  cantnflem1  9649  cnfcom  9660  rankr1ai  9758  rankonidlem  9788  rankxplim2  9840  oncard  9920  ficardom  9921  cardne  9925  acnnum  10012  alephord2i  10037  cardaleph  10049  aceq3lem  10080  dfac5lem5  10087  dfac12lem3  10106  ackbij1lem16  10194  cfslb  10226  cfslb2n  10228  cfsmolem  10230  fin4i  10258  infpssr  10268  fin1a2lem6  10365  axdc3lem2  10411  axcclem  10417  ttukeylem6  10474  fodomb  10486  gchi  10584  pwfseq  10624  inawina  10650  wunfi  10681  inar1  10735  ltexnq  10935  ltbtwnnq  10938  ltexprlem4  10999  ltexpri  11003  prlem936  11007  suplem1pr  11012  suplem2pr  11013  recexsrlem  11063  mulgt0sr  11065  map2psrpr  11070  supsr  11072  eqlei  11291  eqlei2  11292  ledivp1i  12115  nnind  12211  nnmulcl  12217  nn0ge2m1nn  12519  nnnegz  12539  ublbneg  12899  xmulasslem  13252  ixxssixx  13327  iccshftri  13455  iccshftli  13457  iccdili  13459  icccntri  13461  elfz1b  13561  fzo1fzo0n0  13683  elfzonlteqm1  13709  elfzo0l  13724  ssfzo12  13727  fzoopth  13730  elfzo1elm1fzo0  13736  elfzr  13748  elfzlmr  13749  zmodidfzoimp  13870  mptnn0fsuppr  13971  seqp1  13988  seqcl2  13992  seqfveq2  13996  seqshft2  14000  monoord  14004  seqsplit  14007  seqcaopr3  14009  seqf1olem2a  14012  seqf1o  14015  seqid2  14020  seqhomo  14021  hashf1rn  14324  hashinfxadd  14357  hashf1lem2  14428  seqcoll  14436  hash2pr  14441  pr2pwpr  14451  hashge2el2difr  14453  hash3tr  14463  fi1uzind  14479  brfi1indALT  14482  elovmptnn0wrd  14531  swrdswrd  14677  pfxccatin12lem2a  14699  swrdccat  14707  swrdccatin1d  14715  swrdccatin2d  14716  repswccat  14758  cshwidxmod  14775  relexpsucnnr  14998  rtrclreclem3  15033  rtrclreclem4  15034  dfrtrcl2  15035  relexpindlem  15036  relexpind  15037  rtrclind  15038  cjre  15112  climeu  15528  climub  15635  fsum2d  15744  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fsumiun  15794  prodfn0  15867  prodfrec  15868  ntrivcvg  15870  fprodabs  15947  fprod2d  15954  fprodefsum  16068  ruclem9  16213  dvdsmod0  16235  p1modz1  16236  dvdsmodexp  16237  dvdsabseq  16290  mod2eq1n2dvds  16324  mulsucdiv2z  16330  nno  16359  nn0o  16360  sadcadd  16435  sadadd2  16437  saddisjlem  16441  smuval2  16459  smupval  16465  smueqlem  16467  smumullem  16469  dfgcd2  16523  lcmgcdlem  16583  lcmftp  16613  exprmfct  16681  eulerthlem2  16759  dvdsprmpweqnn  16863  dvdsprmpweqle  16864  pcmpt  16870  vdwlem10  16968  cshwsidrepsw  17071  cshwshashlem1  17073  prmlem1a  17084  setsn0fun  17150  ressval3d  17223  mreexexd  17616  letsr  18559  insubm  18752  ghmghmrn  19174  pmtrfrn  19395  pmtr3ncom  19412  gsmtrcl  19453  psgnsn  19457  sylow1lem1  19535  efginvrel2  19664  efgsrel  19671  cntzcmnss  19778  gsum2dlem2  19908  telgsumfzs  19926  dprdval  19942  ablfac1eulem  20011  pgpfac1  20019  pgpfac  20023  srgpcomp  20134  ringrng  20201  ring1ne0  20215  rngimf1o  20370  rngimrnghm  20371  rngimcnv  20372  0ringnnzr  20441  zrhpsgnelbas  21510  psgndiflemA  21517  mplcoe1  21951  mplcoe3  21952  mplcoe5lem  21953  mplcoe5  21954  mpfaddcl  22019  mpfmulcl  22020  coe1ae0  22108  coe1fzgsumd  22198  gsummoncoe1  22202  pf1addcl  22247  pf1mulcl  22248  evl1gsumd  22251  mamufacex  22290  mat0dimcrng  22364  mavmulsolcl  22445  mdetunilem9  22514  cramerlem3  22583  pmatcollpw3fi1  22682  pm2mpfo  22708  chmaidscmat  22742  chfacfscmul0  22752  chfacfpmmul0  22756  cpmadugsumlemF  22770  tg2  22859  neindisj2  23017  neiptopnei  23026  t1t0  23242  fiuncmp  23298  hmeof1o  23658  ist1-5lem  23714  t1r0  23715  alexsublem  23938  imasdsf1olem  24268  tgioo  24691  fsumcn  24768  voliunlem3  25460  itgfsum  25735  dvbsss  25810  dvmptfsum  25886  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem4  25943  plyco  26153  dgrcolem1  26186  dgrco  26188  dvntaylp  26286  taylthlem1  26288  jensen  26906  bposlem5  27206  lgsqrmodndvds  27271  gausslemma2dlem0i  27282  gausslemma2dlem4  27287  lgsquad2lem2  27303  2lgslem3  27322  2lgs  27325  2lgsoddprm  27334  dchrisum0flb  27428  pntpbnd1  27504  pntlemf  27523  madebdayim  27806  oldbdayim  27807  pw2cut  28342  brbtwn  28833  brcgr  28834  umgrnloopv  29040  umgrnloop  29042  usgrnloopvALT  29135  usgrnloopALT  29137  usgredg2vlem2  29160  subgrprop  29207  uvtxnbgrvtx  29327  cusgrsize2inds  29388  rgrprop  29495  rusgrprop  29497  wlkprop  29546  wlkvtxeledg  29559  wlkeq  29569  wlkl1loop  29573  wlk1walk  29574  uspgr2wlkeqi  29583  wlkreslem  29604  wlkres  29605  redwlk  29607  lfgrwlknloop  29624  2pthnloop  29668  usgr2trlncl  29697  usgr2pth  29701  clwlkcompim  29717  clwlkcompbp  29719  uspgrn2crct  29745  crctcshwlkn0  29758  wwlknp  29780  wwlkswwlksn  29802  wlkiswwlks2lem4  29809  wlkiswwlks2  29812  wlklnwwlkln2lem  29819  wwlksnext  29830  wwlksnextbi  29831  wwlksnredwwlkn0  29833  wwlksnextwrd  29834  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlkflem  29940  clwwisshclwws  29951  clwwlknp  29973  clwwlknwwlksn  29974  clwwlkwwlksb  29990  clwwlkext2edg  29992  umgrhashecclwwlk  30014  clwwlknun  30048  1pthond  30080  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  eupth2  30175  3vfriswmgr  30214  3cyclfrgrrn1  30221  n4cyclfrgr  30227  frgrnbnb  30229  frgrncvvdeqlem3  30237  frgrncvvdeqlem6  30240  frgrncvvdeqlem7  30241  frgrncvvdeqlem8  30242  frgrwopreglem4a  30246  frgrwopreg  30259  frgrregorufr0  30260  frgr2wwlkeqm  30267  2clwwlk2clwwlklem  30282  wlkl0  30303  frgrreggt1  30329  frgrregord013  30331  frgrregord13  30332  frgrogt3nreg  30333  friendshipgt3  30334  friendship  30335  blocn2  30744  cvexchlem  32304  cdj3lem2b  32373  nnindf  32751  gsumwun  33012  domnprodn0  33233  issgon  34120  sitgclg  34340  sseqp1  34393  bnj938  34934  bnj964  34940  bnj1052  34972  bnj1125  34989  onvf1odlem4  35100  subfacp1lem6  35179  cvmliftlem7  35285  cvmliftlem10  35288  mclsrcl  35555  pprodss4v  35879  segleantisym  36110  rankeq1o  36166  bj-restv  37090  iooelexlt  37357  relowlssretop  37358  rdgeqoa  37365  matunitlindflem1  37617  poimirlem22  37643  poimirlem25  37646  poimirlem28  37649  poimirlem31  37652  mblfinlem3  37660  mbfresfi  37667  mettrifi  37758  opidon2OLD  37855  isexid2  37856  grpomndo  37876  elghomlem2OLD  37887  rngoidmlem  37937  rngoueqz  37941  iscringd  37999  cdlemk35s  40938  cdlemk39s  40940  cdlemk42  40942  uzindd  41972  mzpadd  42733  mzpmul  42734  mzpcompact2  42747  dford3lem2  43023  aomclem6  43055  cnsrexpcl  43161  ensucne0OLD  43526  pr2cv  43544  relexpss1d  43701  iunrelexpmin1  43704  iunrelexpmin2  43708  tfindsd  44206  nzin  44314  axc11next  44402  iotavalsb  44429  ssdec  45089  fperiodmullem  45308  monoordxrv  45484  fmul01  45585  fmulcl  45586  fmuldfeqlem1  45587  fmuldfeq  45588  iblspltprt  45978  itgspltprt  45984  stoweidlem2  46007  stoweidlem3  46008  stoweidlem6  46011  stoweidlem8  46013  stoweidlem17  46022  stoweidlem19  46024  stoweidlem21  46026  stoweidlem26  46031  stoweidlem31  46036  stoweidlem43  46048  fourierdlem42  46154  funressnfv  47048  eu2ndop1stv  47130  afv0fv0  47154  afv0nbfvbi  47156  funressnbrafv2  47249  funbrafv2  47252  nelbrim  47280  ssfz12  47319  smonoord  47376  iccpartiltu  47427  iccpartigtl  47428  iccelpart  47438  icceuelpart  47441  fargshiftf  47445  fargshiftf1  47446  fargshiftfo  47447  sprel  47489  sprsymrelf1lem  47496  sprsymrelfolem2  47498  prproropf1olem4  47511  lighneallem4  47615  mogoldbblem  47725  fpprnn  47735  fpprwppr  47744  fpprwpprb  47745  sbgoldbwt  47782  bgoldbtbndlem2  47811  bgoldbtbndlem4  47813  tgoldbach  47822  grimprop  47887  grlimprop  47987  grilcbri2  48007  upwlkwlk  48131  clcllaw  48183  intop  48195  clintop  48200  assintop  48201  assintopcllaw  48204  lmod0rng  48221  ztprmneprm  48339  scmsuppss  48363  ply1mulgsumlem1  48379  ply1mulgsumlem2  48380  lcoel0  48421  ellcoellss  48428  lindslinindsimp2lem5  48455  ldepspr  48466  flnn0div2ge  48526  nnolog2flm1  48583  blengt1fldiv2p1  48586  dignn0flhalf  48611  naryfvalelfv  48625  0aryfvalelfv  48628  fv1arycl  48630  fv2arycl  48641