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  665  axc16i  2433  mo4  2558  sbcn1  3833  sbcim1  3834  sbcim1OLD  3835  sbcbi1  3839  sbcel21v  3851  csbie2df  4441  elimasni  6091  sotri  6129  unixpid  6284  f0rn0  6777  f1ocnv  6846  funbrfv  6943  elfvmptrab1w  7025  f1dom3el3dif  7272  oprabidw  7444  oprabid  7445  oprabv  7473  ndmovordi  7602  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  elovmpt3rab1  7670  limomss  7864  unielxp  8017  bropfvvvvlem  8081  f1o2ndf1  8112  smogt  8371  tfrlem1  8380  oawordeulem  8558  omass  8584  ecopovtrn  8818  mapfvd  8877  findcard2d  9170  ssfi  9177  f1domfi  9188  php  9214  phpOLD  9226  unxpdom  9257  findcard3  9289  findcard3OLD  9290  isfinite2  9305  fsuppimp  9372  fsuppunfi  9387  fsuppunbi  9388  fsuppres  9392  infsupprpr  9503  cantnfval2  9668  cantnfle  9670  cantnfp1lem3  9679  cantnflem1  9688  cnfcom  9699  rankr1ai  9797  rankonidlem  9827  rankxplim2  9879  oncard  9959  ficardom  9960  cardne  9964  acnnum  10051  alephord2i  10076  cardaleph  10088  aceq3lem  10119  dfac5lem5  10126  dfac12lem3  10144  ackbij1lem16  10234  cfslb  10265  cfslb2n  10267  cfsmolem  10269  fin4i  10297  infpssr  10307  fin1a2lem6  10404  axdc3lem2  10450  axcclem  10456  ttukeylem6  10513  fodomb  10525  gchi  10623  fpwwe2lem4  10633  pwfseqlem4  10661  pwfseq  10663  inawina  10689  wunfi  10720  inar1  10774  ltexnq  10974  ltbtwnnq  10977  ltexprlem4  11038  ltexpri  11042  prlem936  11046  suplem1pr  11051  suplem2pr  11052  recexsrlem  11102  mulgt0sr  11104  map2psrpr  11109  supsr  11111  eqlei  11330  eqlei2  11331  ledivp1i  12145  nnind  12236  nnmulcl  12242  nn0ge2m1nn  12547  nnnegz  12567  ublbneg  12923  xmulasslem  13270  ixxssixx  13344  iccshftri  13470  iccshftli  13472  iccdili  13474  icccntri  13476  elfz1b  13576  fzo1fzo0n0  13689  elfzonlteqm1  13714  elfzo0l  13728  ssfzo12  13731  elfzo1elm1fzo0  13739  elfzr  13751  elfzlmr  13752  zmodidfzoimp  13872  mptnn0fsuppr  13970  seqp1  13987  seqcl2  13992  seqfveq2  13996  seqshft2  14000  monoord  14004  seqsplit  14007  seqcaopr3  14009  seqf1olem2a  14012  seqf1o  14015  seqid2  14020  seqhomo  14021  hashf1rn  14318  hashinfxadd  14351  hashf1lem2  14423  seqcoll  14431  hash2pr  14436  pr2pwpr  14446  hashge2el2difr  14448  hash3tr  14457  fi1uzind  14464  brfi1indALT  14467  elovmptnn0wrd  14515  swrdswrd  14661  pfxccatin12lem2a  14683  swrdccat  14691  swrdccatin1d  14699  swrdccatin2d  14700  repswccat  14742  cshwidxmod  14759  relexpsucnnr  14978  rtrclreclem3  15013  rtrclreclem4  15014  dfrtrcl2  15015  relexpindlem  15016  relexpind  15017  rtrclind  15018  cjre  15092  climeu  15505  climub  15614  fsum2d  15723  fsumabs  15753  fsumrlim  15763  fsumo1  15764  fsumiun  15773  prodfn0  15846  prodfrec  15847  ntrivcvg  15849  fprodabs  15924  fprod2d  15931  fprodefsum  16044  ruclem9  16187  dvdsmod0  16209  p1modz1  16210  dvdsmodexp  16211  dvdsabseq  16262  mod2eq1n2dvds  16296  mulsucdiv2z  16302  nno  16331  nn0o  16332  sadcadd  16405  sadadd2  16407  saddisjlem  16411  smuval2  16429  smupval  16435  smueqlem  16437  smumullem  16439  dfgcd2  16494  lcmgcdlem  16549  lcmftp  16579  exprmfct  16647  eulerthlem2  16721  dvdsprmpweqnn  16824  dvdsprmpweqle  16825  pcmpt  16831  vdwlem10  16929  cshwsidrepsw  17033  cshwshashlem1  17035  prmlem1a  17046  setsn0fun  17112  ressval3d  17197  ressval3dOLD  17198  mreexexd  17598  letsr  18552  insubm  18737  ghmghmrn  19151  pmtrfrn  19369  pmtr3ncom  19386  gsmtrcl  19427  psgnsn  19431  sylow1lem1  19509  efginvrel2  19638  efgsrel  19645  cntzcmnss  19752  gsum2dlem2  19882  telgsumfzs  19900  dprdval  19916  ablfac1eulem  19985  pgpfac1  19993  pgpfac  19997  srgpcomp  20114  ringrng  20175  ring1ne0  20189  rngimf1o  20347  rngimrnghm  20348  rngimcnv  20349  0ringnnzr  20416  zrhpsgnelbas  21368  psgndiflemA  21375  mplcoe1  21813  mplcoe3  21814  mplcoe5lem  21815  mplcoe5  21816  mpfaddcl  21889  mpfmulcl  21890  coe1ae0  21961  coe1fzgsumd  22048  gsummoncoe1  22050  pf1addcl  22094  pf1mulcl  22095  evl1gsumd  22098  mamufacex  22113  mat0dimcrng  22194  mavmulsolcl  22275  mdetunilem9  22344  cramerlem3  22413  pmatcollpw3fi1  22512  pm2mpfo  22538  chmaidscmat  22572  chfacfscmul0  22582  chfacfpmmul0  22586  cpmadugsumlemF  22600  tg2  22690  neindisj2  22849  neiptopnei  22858  t1t0  23074  fiuncmp  23130  hmeof1o  23490  ist1-5lem  23546  t1r0  23547  alexsublem  23770  imasdsf1olem  24101  tgioo  24534  fsumcn  24610  voliunlem3  25303  itgfsum  25578  dvbsss  25653  dvmptfsum  25726  dvfsumlem2  25778  dvfsumlem4  25780  plyco  25989  dgrcolem1  26021  dgrco  26023  dvntaylp  26117  taylthlem1  26119  jensen  26727  bposlem5  27025  lgsqrmodndvds  27090  gausslemma2dlem0i  27101  gausslemma2dlem4  27106  lgsquad2lem2  27122  2lgslem3  27141  2lgs  27144  2lgsoddprm  27153  dchrisum0flb  27247  pntpbnd1  27323  pntlemf  27342  madebdayim  27617  oldbdayim  27618  brbtwn  28422  brcgr  28423  umgrnloopv  28631  umgrnloop  28633  usgrnloopvALT  28723  usgrnloopALT  28725  usgredg2vlem2  28748  subgrprop  28795  uvtxnbgrvtx  28915  cusgrsize2inds  28975  rgrprop  29082  rusgrprop  29084  wlkprop  29133  wlkvtxeledg  29146  wlkeq  29156  wlkl1loop  29160  wlk1walk  29161  uspgr2wlkeqi  29170  wlkreslem  29191  wlkres  29192  redwlk  29194  lfgrwlknloop  29211  2pthnloop  29253  usgr2trlncl  29282  usgr2pth  29286  clwlkcompim  29302  clwlkcompbp  29304  uspgrn2crct  29327  crctcshwlkn0  29340  wwlknp  29362  wwlkswwlksn  29384  wlkiswwlks2lem4  29391  wlkiswwlks2  29394  wlklnwwlkln2lem  29401  wwlksnext  29412  wwlksnextbi  29413  wwlksnredwwlkn0  29415  wwlksnextwrd  29416  clwlkclwwlklem2a  29516  clwlkclwwlklem2  29518  clwlkclwwlkflem  29522  clwwisshclwws  29533  clwwlknp  29555  clwwlknwwlksn  29556  clwwlkwwlksb  29572  clwwlkext2edg  29574  umgrhashecclwwlk  29596  clwwlknun  29630  1pthond  29662  upgr3v3e3cycl  29698  upgr4cycl4dv4e  29703  eupth2  29757  3vfriswmgr  29796  3cyclfrgrrn1  29803  n4cyclfrgr  29809  frgrnbnb  29811  frgrncvvdeqlem3  29819  frgrncvvdeqlem6  29822  frgrncvvdeqlem7  29823  frgrncvvdeqlem8  29824  frgrwopreglem4a  29828  frgrwopreg  29841  frgrregorufr0  29842  frgr2wwlkeqm  29849  2clwwlk2clwwlklem  29864  wlkl0  29885  frgrreggt1  29911  frgrregord013  29913  frgrregord13  29914  frgrogt3nreg  29915  friendshipgt3  29916  friendship  29917  blocn2  30326  cvexchlem  31886  cdj3lem2b  31955  cnvoprabOLD  32210  nnindf  32290  issgon  33417  sitgclg  33637  sseqp1  33690  bnj938  34244  bnj964  34250  bnj1052  34282  bnj1125  34299  subfacp1lem6  34472  cvmliftlem7  34578  cvmliftlem10  34581  mclsrcl  34848  pprodss4v  35158  segleantisym  35389  rankeq1o  35445  gg-dvfsumlem2  35471  bj-restv  36281  iooelexlt  36548  relowlssretop  36549  rdgeqoa  36556  matunitlindflem1  36789  poimirlem22  36815  poimirlem25  36818  poimirlem28  36821  poimirlem31  36824  mblfinlem3  36832  mbfresfi  36839  mettrifi  36930  opidon2OLD  37027  isexid2  37028  grpomndo  37048  elghomlem2OLD  37059  rngoidmlem  37109  rngoueqz  37113  iscringd  37171  cdlemk35s  40113  cdlemk39s  40115  cdlemk42  40117  uzindd  41150  mzpadd  41780  mzpmul  41781  mzpcompact2  41794  dford3lem2  42070  aomclem6  42105  cnsrexpcl  42211  ensucne0OLD  42585  pr2cv  42603  relexpss1d  42760  iunrelexpmin1  42763  iunrelexpmin2  42767  tfindsd  43268  nzin  43381  axc11next  43469  iotavalsb  43496  ssdec  44080  fperiodmullem  44313  monoordxrv  44492  fmul01  44596  fmulcl  44597  fmuldfeqlem1  44598  fmuldfeq  44599  fprodcnlem  44615  iblspltprt  44989  itgspltprt  44995  stoweidlem2  45018  stoweidlem3  45019  stoweidlem6  45022  stoweidlem8  45024  stoweidlem17  45033  stoweidlem19  45035  stoweidlem21  45037  stoweidlem26  45042  stoweidlem31  45047  stoweidlem43  45059  fourierdlem42  45165  funressnfv  46053  eu2ndop1stv  46133  afv0fv0  46157  afv0nbfvbi  46159  funressnbrafv2  46252  funbrafv2  46255  nelbrim  46283  ssfz12  46322  fzoopth  46335  smonoord  46339  iccpartiltu  46390  iccpartigtl  46391  iccelpart  46401  icceuelpart  46404  fargshiftf  46408  fargshiftf1  46409  fargshiftfo  46410  sprel  46452  sprsymrelf1lem  46459  sprsymrelfolem2  46461  prproropf1olem4  46474  lighneallem4  46578  mogoldbblem  46688  fpprnn  46698  fpprwppr  46707  fpprwpprb  46708  sbgoldbwt  46745  bgoldbtbndlem2  46774  bgoldbtbndlem4  46776  tgoldbach  46785  upwlkwlk  46817  clcllaw  46869  intop  46881  clintop  46886  assintop  46887  assintopcllaw  46890  lmod0rng  46910  ztprmneprm  47113  scmsuppss  47138  ply1mulgsumlem1  47156  ply1mulgsumlem2  47157  lcoel0  47198  ellcoellss  47205  lindslinindsimp2lem5  47232  ldepspr  47243  flnn0div2ge  47308  nnolog2flm1  47365  blengt1fldiv2p1  47368  dignn0flhalf  47393  naryfvalelfv  47407  0aryfvalelfv  47410  fv1arycl  47412  fv2arycl  47423