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  2565  sbcn1  3749  sbcim1  3750  sbcim1OLD  3751  sbcbi1  3756  sbcel21v  3768  csbie2df  4355  elimasni  5959  sotri  5992  unixpid  6147  f0rn0  6604  f1ocnv  6673  funbrfv  6763  elfvmptrab1w  6844  f1dom3el3dif  7081  oprabidw  7244  oprabid  7245  oprabv  7271  ndmovordi  7399  elovmporab  7451  elovmporab1w  7452  elovmporab1  7453  elovmpt3rab1  7465  limomss  7649  unielxp  7799  bropfvvvvlem  7859  f1o2ndf1  7891  smogt  8104  tfrlem1  8112  oawordeulem  8282  omass  8308  ecopovtrn  8502  mapfvd  8560  php  8830  findcard2d  8844  ssfi  8851  unxpdom  8885  findcard3  8914  isfinite2  8929  fsuppimp  8991  fsuppunfi  9005  fsuppunbi  9006  fsuppres  9010  infsupprpr  9120  cantnfval2  9284  cantnfle  9286  cantnfp1lem3  9295  cantnflem1  9304  cnfcom  9315  rankr1ai  9414  rankonidlem  9444  rankxplim2  9496  oncard  9576  ficardom  9577  cardne  9581  acnnum  9666  alephord2i  9691  cardaleph  9703  aceq3lem  9734  dfac5lem5  9741  dfac12lem3  9759  ackbij1lem16  9849  cfslb  9880  cfslb2n  9882  cfsmolem  9884  fin4i  9912  infpssr  9922  fin1a2lem6  10019  axdc3lem2  10065  axcclem  10071  ttukeylem6  10128  fodomb  10140  gchi  10238  fpwwe2lem4  10248  pwfseqlem4  10276  pwfseq  10278  inawina  10304  wunfi  10335  inar1  10389  ltexnq  10589  ltbtwnnq  10592  ltexprlem4  10653  ltexpri  10657  prlem936  10661  suplem1pr  10666  suplem2pr  10667  recexsrlem  10717  mulgt0sr  10719  map2psrpr  10724  supsr  10726  eqlei  10942  eqlei2  10943  ledivp1i  11757  nnind  11848  nnmulcl  11854  nn0ge2m1nn  12159  nnnegz  12179  ublbneg  12529  xmulasslem  12875  ixxssixx  12949  iccshftri  13075  iccshftli  13077  iccdili  13079  icccntri  13081  elfz1b  13181  fzo1fzo0n0  13293  elfzonlteqm1  13318  elfzo0l  13332  ssfzo12  13335  elfzo1elm1fzo0  13343  elfzr  13355  elfzlmr  13356  zmodidfzoimp  13474  mptnn0fsuppr  13572  seqp1  13589  seqcl2  13594  seqfveq2  13598  seqshft2  13602  monoord  13606  seqsplit  13609  seqcaopr3  13611  seqf1olem2a  13614  seqf1o  13617  seqid2  13622  seqhomo  13623  hashf1rn  13919  hashinfxadd  13952  hashf1lem2  14022  seqcoll  14030  hash2pr  14035  pr2pwpr  14045  hashge2el2difr  14047  hash3tr  14056  fi1uzind  14063  brfi1indALT  14066  elovmptnn0wrd  14114  swrdswrd  14270  pfxccatin12lem2a  14292  swrdccat  14300  swrdccatin1d  14308  swrdccatin2d  14309  repswccat  14351  cshwidxmod  14368  relexpsucnnr  14588  rtrclreclem3  14623  rtrclreclem4  14624  dfrtrcl2  14625  relexpindlem  14626  relexpind  14627  rtrclind  14628  cjre  14702  climeu  15116  climub  15225  fsum2d  15335  fsumabs  15365  fsumrlim  15375  fsumo1  15376  fsumiun  15385  prodfn0  15458  prodfrec  15459  ntrivcvg  15461  fprodabs  15536  fprod2d  15543  fprodefsum  15656  ruclem9  15799  dvdsmod0  15821  p1modz1  15822  dvdsmodexp  15823  dvdsabseq  15874  mod2eq1n2dvds  15908  mulsucdiv2z  15914  nno  15943  nn0o  15944  sadcadd  16017  sadadd2  16019  saddisjlem  16023  smuval2  16041  smupval  16047  smueqlem  16049  smumullem  16051  dfgcd2  16106  lcmgcdlem  16163  lcmftp  16193  exprmfct  16261  eulerthlem2  16335  dvdsprmpweqnn  16438  dvdsprmpweqle  16439  pcmpt  16445  vdwlem10  16543  cshwsidrepsw  16647  cshwshashlem1  16649  prmlem1a  16660  setsn0fun  16726  ressval3d  16798  mreexexd  17151  letsr  18099  insubm  18245  ghmghmrn  18641  pmtrfrn  18850  pmtr3ncom  18867  gsmtrcl  18908  psgnsn  18912  sylow1lem1  18987  efginvrel2  19117  efgsrel  19124  cntzcmnss  19226  gsum2dlem2  19356  telgsumfzs  19374  dprdval  19390  ablfac1eulem  19459  pgpfac1  19467  pgpfac  19471  srgpcomp  19547  ring1ne0  19609  rimf1o  19754  rimrhm  19755  brric2  19765  0ringnnzr  20307  zrhpsgnelbas  20556  psgndiflemA  20563  mplcoe1  20994  mplcoe3  20995  mplcoe5lem  20996  mplcoe5  20997  mpfaddcl  21065  mpfmulcl  21066  coe1ae0  21137  coe1fzgsumd  21223  gsummoncoe1  21225  pf1addcl  21269  pf1mulcl  21270  evl1gsumd  21273  mamufacex  21288  mat0dimcrng  21367  mavmulsolcl  21448  mdetunilem9  21517  cramerlem3  21586  pmatcollpw3fi1  21685  pm2mpfo  21711  chmaidscmat  21745  chfacfscmul0  21755  chfacfpmmul0  21759  cpmadugsumlemF  21773  tg2  21862  neindisj2  22020  neiptopnei  22029  t1t0  22245  fiuncmp  22301  hmeof1o  22661  ist1-5lem  22717  t1r0  22718  alexsublem  22941  imasdsf1olem  23271  tgioo  23693  fsumcn  23767  voliunlem3  24449  itgfsum  24724  dvbsss  24799  dvmptfsum  24872  dvfsumlem2  24924  dvfsumlem4  24926  plyco  25135  dgrcolem1  25167  dgrco  25169  dvntaylp  25263  taylthlem1  25265  jensen  25871  bposlem5  26169  lgsqrmodndvds  26234  gausslemma2dlem0i  26245  gausslemma2dlem4  26250  lgsquad2lem2  26266  2lgslem3  26285  2lgs  26288  2lgsoddprm  26297  dchrisum0flb  26391  pntpbnd1  26467  pntlemf  26486  brbtwn  26990  brcgr  26991  umgrnloopv  27197  umgrnloop  27199  usgrnloopvALT  27289  usgrnloopALT  27291  usgredg2vlem2  27314  subgrprop  27361  uvtxnbgrvtx  27481  cusgrsize2inds  27541  rgrprop  27648  rusgrprop  27650  wlkprop  27699  wlkvtxeledg  27711  wlkeq  27721  wlkl1loop  27725  wlk1walk  27726  uspgr2wlkeqi  27735  wlkreslem  27757  wlkres  27758  redwlk  27760  lfgrwlknloop  27777  2pthnloop  27818  usgr2trlncl  27847  usgr2pth  27851  clwlkcompim  27867  clwlkcompbp  27869  uspgrn2crct  27892  crctcshwlkn0  27905  wwlknp  27927  wwlkswwlksn  27949  wlkiswwlks2lem4  27956  wlkiswwlks2  27959  wlklnwwlkln2lem  27966  wwlksnext  27977  wwlksnextbi  27978  wwlksnredwwlkn0  27980  wwlksnextwrd  27981  clwlkclwwlklem2a  28081  clwlkclwwlklem2  28083  clwlkclwwlkflem  28087  clwwisshclwws  28098  clwwlknp  28120  clwwlknwwlksn  28121  clwwlkwwlksb  28137  clwwlkext2edg  28139  umgrhashecclwwlk  28161  clwwlknun  28195  1pthond  28227  upgr3v3e3cycl  28263  upgr4cycl4dv4e  28268  eupth2  28322  3vfriswmgr  28361  3cyclfrgrrn1  28368  n4cyclfrgr  28374  frgrnbnb  28376  frgrncvvdeqlem3  28384  frgrncvvdeqlem6  28387  frgrncvvdeqlem7  28388  frgrncvvdeqlem8  28389  frgrwopreglem4a  28393  frgrwopreg  28406  frgrregorufr0  28407  frgr2wwlkeqm  28414  2clwwlk2clwwlklem  28429  wlkl0  28450  frgrreggt1  28476  frgrregord013  28478  frgrregord13  28479  frgrogt3nreg  28480  friendshipgt3  28481  friendship  28482  blocn2  28889  cvexchlem  30449  cdj3lem2b  30518  cnvoprabOLD  30775  nnindf  30853  issgon  31803  sitgclg  32021  sseqp1  32074  bnj938  32630  bnj964  32636  bnj1052  32668  bnj1125  32685  subfacp1lem6  32860  cvmliftlem7  32966  cvmliftlem10  32969  mclsrcl  33236  madebdayim  33807  oldbdayim  33808  pprodss4v  33923  segleantisym  34154  rankeq1o  34210  bj-restv  35001  iooelexlt  35270  relowlssretop  35271  rdgeqoa  35278  matunitlindflem1  35510  poimirlem22  35536  poimirlem25  35539  poimirlem28  35542  poimirlem31  35545  mblfinlem3  35553  mbfresfi  35560  mettrifi  35652  opidon2OLD  35749  isexid2  35750  grpomndo  35770  elghomlem2OLD  35781  rngoidmlem  35831  rngoueqz  35835  iscringd  35893  cdlemk35s  38688  cdlemk39s  38690  cdlemk42  38692  uzindd  39719  mzpadd  40263  mzpmul  40264  mzpcompact2  40277  dford3lem2  40552  aomclem6  40587  cnsrexpcl  40693  ensucne0OLD  40822  pr2cv  40831  relexpss1d  40990  iunrelexpmin1  40993  iunrelexpmin2  40997  tfindsd  41501  nzin  41609  axc11next  41697  iotavalsb  41724  ssdec  42311  fperiodmullem  42515  monoordxrv  42697  fmul01  42796  fmulcl  42797  fmuldfeqlem1  42798  fmuldfeq  42799  fprodcnlem  42815  iblspltprt  43189  itgspltprt  43195  stoweidlem2  43218  stoweidlem3  43219  stoweidlem6  43222  stoweidlem8  43224  stoweidlem17  43233  stoweidlem19  43235  stoweidlem21  43237  stoweidlem26  43242  stoweidlem31  43247  stoweidlem43  43259  fourierdlem42  43365  funressnfv  44209  eu2ndop1stv  44289  afv0fv0  44313  afv0nbfvbi  44315  funressnbrafv2  44408  funbrafv2  44411  nelbrim  44439  ssfz12  44479  fzoopth  44492  smonoord  44496  iccpartiltu  44547  iccpartigtl  44548  iccelpart  44558  icceuelpart  44561  fargshiftf  44565  fargshiftf1  44566  fargshiftfo  44567  sprel  44609  sprsymrelf1lem  44616  sprsymrelfolem2  44618  prproropf1olem4  44631  lighneallem4  44735  mogoldbblem  44845  fpprnn  44855  fpprwppr  44864  fpprwpprb  44865  sbgoldbwt  44902  bgoldbtbndlem2  44931  bgoldbtbndlem4  44933  tgoldbach  44942  upwlkwlk  44974  clcllaw  45058  intop  45070  clintop  45075  assintop  45076  assintopcllaw  45079  lmod0rng  45099  ringrng  45110  rngimf1o  45136  rngimrnghm  45137  ztprmneprm  45356  scmsuppss  45381  ply1mulgsumlem1  45400  ply1mulgsumlem2  45401  lcoel0  45442  ellcoellss  45449  lindslinindsimp2lem5  45476  ldepspr  45487  flnn0div2ge  45552  nnolog2flm1  45609  blengt1fldiv2p1  45612  dignn0flhalf  45637  naryfvalelfv  45651  0aryfvalelfv  45654  fv1arycl  45656  fv2arycl  45667