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  668  axc16i  2444  mo4  2569  sbcn1  3860  sbcim1  3861  sbcim1OLD  3862  sbcbi1  3866  sbcel21v  3877  sbccomlem  3891  csbie2df  4466  elimasni  6121  sotri  6159  unixpid  6315  f0rn0  6806  f1ocnv  6874  funbrfv  6971  elfvmptrab1w  7056  f1dom3el3dif  7306  oprabidw  7479  oprabid  7480  oprabv  7510  ndmovordi  7641  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  elovmpt3rab1  7710  limomss  7908  unielxp  8068  bropfvvvvlem  8132  f1o2ndf1  8163  smogt  8423  tfrlem1  8432  oawordeulem  8610  omass  8636  ecopovtrn  8878  mapfvd  8937  findcard2d  9232  ssfi  9240  f1domfi  9247  php  9273  phpOLD  9285  unxpdom  9316  findcard3  9346  findcard3OLD  9347  isfinite2  9362  fsuppimp  9438  fsuppunfi  9457  fsuppunbi  9458  fsuppres  9462  infsupprpr  9573  cantnfval2  9738  cantnfle  9740  cantnfp1lem3  9749  cantnflem1  9758  cnfcom  9769  rankr1ai  9867  rankonidlem  9897  rankxplim2  9949  oncard  10029  ficardom  10030  cardne  10034  acnnum  10121  alephord2i  10146  cardaleph  10158  aceq3lem  10189  dfac5lem5  10196  dfac12lem3  10215  ackbij1lem16  10303  cfslb  10335  cfslb2n  10337  cfsmolem  10339  fin4i  10367  infpssr  10377  fin1a2lem6  10474  axdc3lem2  10520  axcclem  10526  ttukeylem6  10583  fodomb  10595  gchi  10693  pwfseq  10733  inawina  10759  wunfi  10790  inar1  10844  ltexnq  11044  ltbtwnnq  11047  ltexprlem4  11108  ltexpri  11112  prlem936  11116  suplem1pr  11121  suplem2pr  11122  recexsrlem  11172  mulgt0sr  11174  map2psrpr  11179  supsr  11181  eqlei  11400  eqlei2  11401  ledivp1i  12220  nnind  12311  nnmulcl  12317  nn0ge2m1nn  12622  nnnegz  12642  ublbneg  12998  xmulasslem  13347  ixxssixx  13421  iccshftri  13547  iccshftli  13549  iccdili  13551  icccntri  13553  elfz1b  13653  fzo1fzo0n0  13767  elfzonlteqm1  13792  elfzo0l  13806  ssfzo12  13809  fzoopth  13812  elfzo1elm1fzo0  13818  elfzr  13830  elfzlmr  13831  zmodidfzoimp  13952  mptnn0fsuppr  14050  seqp1  14067  seqcl2  14071  seqfveq2  14075  seqshft2  14079  monoord  14083  seqsplit  14086  seqcaopr3  14088  seqf1olem2a  14091  seqf1o  14094  seqid2  14099  seqhomo  14100  hashf1rn  14401  hashinfxadd  14434  hashf1lem2  14505  seqcoll  14513  hash2pr  14518  pr2pwpr  14528  hashge2el2difr  14530  hash3tr  14540  fi1uzind  14556  brfi1indALT  14559  elovmptnn0wrd  14607  swrdswrd  14753  pfxccatin12lem2a  14775  swrdccat  14783  swrdccatin1d  14791  swrdccatin2d  14792  repswccat  14834  cshwidxmod  14851  relexpsucnnr  15074  rtrclreclem3  15109  rtrclreclem4  15110  dfrtrcl2  15111  relexpindlem  15112  relexpind  15113  rtrclind  15114  cjre  15188  climeu  15601  climub  15710  fsum2d  15819  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  prodfn0  15942  prodfrec  15943  ntrivcvg  15945  fprodabs  16022  fprod2d  16029  fprodefsum  16143  ruclem9  16286  dvdsmod0  16308  p1modz1  16309  dvdsmodexp  16310  dvdsabseq  16361  mod2eq1n2dvds  16395  mulsucdiv2z  16401  nno  16430  nn0o  16431  sadcadd  16504  sadadd2  16506  saddisjlem  16510  smuval2  16528  smupval  16534  smueqlem  16536  smumullem  16538  dfgcd2  16593  lcmgcdlem  16653  lcmftp  16683  exprmfct  16751  eulerthlem2  16829  dvdsprmpweqnn  16932  dvdsprmpweqle  16933  pcmpt  16939  vdwlem10  17037  cshwsidrepsw  17141  cshwshashlem1  17143  prmlem1a  17154  setsn0fun  17220  ressval3d  17305  ressval3dOLD  17306  mreexexd  17706  letsr  18663  insubm  18853  ghmghmrn  19275  pmtrfrn  19500  pmtr3ncom  19517  gsmtrcl  19558  psgnsn  19562  sylow1lem1  19640  efginvrel2  19769  efgsrel  19776  cntzcmnss  19883  gsum2dlem2  20013  telgsumfzs  20031  dprdval  20047  ablfac1eulem  20116  pgpfac1  20124  pgpfac  20128  srgpcomp  20245  ringrng  20308  ring1ne0  20322  rngimf1o  20480  rngimrnghm  20481  rngimcnv  20482  0ringnnzr  20551  zrhpsgnelbas  21635  psgndiflemA  21642  mplcoe1  22078  mplcoe3  22079  mplcoe5lem  22080  mplcoe5  22081  mpfaddcl  22152  mpfmulcl  22153  coe1ae0  22239  coe1fzgsumd  22329  gsummoncoe1  22333  pf1addcl  22378  pf1mulcl  22379  evl1gsumd  22382  mamufacex  22421  mat0dimcrng  22497  mavmulsolcl  22578  mdetunilem9  22647  cramerlem3  22716  pmatcollpw3fi1  22815  pm2mpfo  22841  chmaidscmat  22875  chfacfscmul0  22885  chfacfpmmul0  22889  cpmadugsumlemF  22903  tg2  22993  neindisj2  23152  neiptopnei  23161  t1t0  23377  fiuncmp  23433  hmeof1o  23793  ist1-5lem  23849  t1r0  23850  alexsublem  24073  imasdsf1olem  24404  tgioo  24837  fsumcn  24913  voliunlem3  25606  itgfsum  25882  dvbsss  25957  dvmptfsum  26033  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem4  26090  plyco  26300  dgrcolem1  26333  dgrco  26335  dvntaylp  26431  taylthlem1  26433  jensen  27050  bposlem5  27350  lgsqrmodndvds  27415  gausslemma2dlem0i  27426  gausslemma2dlem4  27431  lgsquad2lem2  27447  2lgslem3  27466  2lgs  27469  2lgsoddprm  27478  dchrisum0flb  27572  pntpbnd1  27648  pntlemf  27667  madebdayim  27944  oldbdayim  27945  pw2cut  28438  brbtwn  28932  brcgr  28933  umgrnloopv  29141  umgrnloop  29143  usgrnloopvALT  29236  usgrnloopALT  29238  usgredg2vlem2  29261  subgrprop  29308  uvtxnbgrvtx  29428  cusgrsize2inds  29489  rgrprop  29596  rusgrprop  29598  wlkprop  29647  wlkvtxeledg  29660  wlkeq  29670  wlkl1loop  29674  wlk1walk  29675  uspgr2wlkeqi  29684  wlkreslem  29705  wlkres  29706  redwlk  29708  lfgrwlknloop  29725  2pthnloop  29767  usgr2trlncl  29796  usgr2pth  29800  clwlkcompim  29816  clwlkcompbp  29818  uspgrn2crct  29841  crctcshwlkn0  29854  wwlknp  29876  wwlkswwlksn  29898  wlkiswwlks2lem4  29905  wlkiswwlks2  29908  wlklnwwlkln2lem  29915  wwlksnext  29926  wwlksnextbi  29927  wwlksnredwwlkn0  29929  wwlksnextwrd  29930  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlkflem  30036  clwwisshclwws  30047  clwwlknp  30069  clwwlknwwlksn  30070  clwwlkwwlksb  30086  clwwlkext2edg  30088  umgrhashecclwwlk  30110  clwwlknun  30144  1pthond  30176  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eupth2  30271  3vfriswmgr  30310  3cyclfrgrrn1  30317  n4cyclfrgr  30323  frgrnbnb  30325  frgrncvvdeqlem3  30333  frgrncvvdeqlem6  30336  frgrncvvdeqlem7  30337  frgrncvvdeqlem8  30338  frgrwopreglem4a  30342  frgrwopreg  30355  frgrregorufr0  30356  frgr2wwlkeqm  30363  2clwwlk2clwwlklem  30378  wlkl0  30399  frgrreggt1  30425  frgrregord013  30427  frgrregord13  30428  frgrogt3nreg  30429  friendshipgt3  30430  friendship  30431  blocn2  30840  cvexchlem  32400  cdj3lem2b  32469  cnvoprabOLD  32734  nnindf  32823  domnprodn0  33247  issgon  34087  sitgclg  34307  sseqp1  34360  bnj938  34913  bnj964  34919  bnj1052  34951  bnj1125  34968  subfacp1lem6  35153  cvmliftlem7  35259  cvmliftlem10  35262  mclsrcl  35529  pprodss4v  35848  segleantisym  36079  rankeq1o  36135  bj-restv  37061  iooelexlt  37328  relowlssretop  37329  rdgeqoa  37336  matunitlindflem1  37576  poimirlem22  37602  poimirlem25  37605  poimirlem28  37608  poimirlem31  37611  mblfinlem3  37619  mbfresfi  37626  mettrifi  37717  opidon2OLD  37814  isexid2  37815  grpomndo  37835  elghomlem2OLD  37846  rngoidmlem  37896  rngoueqz  37900  iscringd  37958  cdlemk35s  40894  cdlemk39s  40896  cdlemk42  40898  uzindd  41933  mzpadd  42694  mzpmul  42695  mzpcompact2  42708  dford3lem2  42984  aomclem6  43016  cnsrexpcl  43122  ensucne0OLD  43492  pr2cv  43510  relexpss1d  43667  iunrelexpmin1  43670  iunrelexpmin2  43674  tfindsd  44174  nzin  44287  axc11next  44375  iotavalsb  44402  ssdec  44990  fperiodmullem  45218  monoordxrv  45397  fmul01  45501  fmulcl  45502  fmuldfeqlem1  45503  fmuldfeq  45504  iblspltprt  45894  itgspltprt  45900  stoweidlem2  45923  stoweidlem3  45924  stoweidlem6  45927  stoweidlem8  45929  stoweidlem17  45938  stoweidlem19  45940  stoweidlem21  45942  stoweidlem26  45947  stoweidlem31  45952  stoweidlem43  45964  fourierdlem42  46070  funressnfv  46958  eu2ndop1stv  47040  afv0fv0  47064  afv0nbfvbi  47066  funressnbrafv2  47159  funbrafv2  47162  nelbrim  47190  ssfz12  47229  smonoord  47245  iccpartiltu  47296  iccpartigtl  47297  iccelpart  47307  icceuelpart  47310  fargshiftf  47314  fargshiftf1  47315  fargshiftfo  47316  sprel  47358  sprsymrelf1lem  47365  sprsymrelfolem2  47367  prproropf1olem4  47380  lighneallem4  47484  mogoldbblem  47594  fpprnn  47604  fpprwppr  47613  fpprwpprb  47614  sbgoldbwt  47651  bgoldbtbndlem2  47680  bgoldbtbndlem4  47682  tgoldbach  47691  grimprop  47753  grlimprop  47808  grilcbri2  47828  upwlkwlk  47862  clcllaw  47914  intop  47926  clintop  47931  assintop  47932  assintopcllaw  47935  lmod0rng  47952  ztprmneprm  48072  scmsuppss  48097  ply1mulgsumlem1  48115  ply1mulgsumlem2  48116  lcoel0  48157  ellcoellss  48164  lindslinindsimp2lem5  48191  ldepspr  48202  flnn0div2ge  48267  nnolog2flm1  48324  blengt1fldiv2p1  48327  dignn0flhalf  48352  naryfvalelfv  48366  0aryfvalelfv  48369  fv1arycl  48371  fv2arycl  48382