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  670  axc16i  2440  mo4  2566  sbcn1  3781  sbcim1  3782  sbcbi1  3786  sbcel21v  3796  sbccomlem  3807  csbie2df  4383  elimasni  6056  sotri  6090  unixpid  6248  f0rn0  6725  f1ocnv  6792  funbrfv  6888  elfvmptrab1w  6975  f1dom3el3dif  7224  oprabidw  7398  oprabid  7399  oprabv  7427  ndmovordi  7558  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  elovmpt3rab1  7627  limomss  7822  unielxp  7980  bropfvvvvlem  8041  f1o2ndf1  8072  smogt  8307  tfrlem1  8315  oawordeulem  8489  omass  8515  ecopovtrn  8767  mapfvd  8827  findcard2d  9101  ssfi  9107  f1domfi  9115  php  9141  unxpdom  9169  findcard3  9193  isfinite2  9208  fsuppimp  9281  fsuppunfi  9301  fsuppunbi  9302  fsuppres  9306  infsupprpr  9419  cantnfval2  9590  cantnfle  9592  cantnfp1lem3  9601  cantnflem1  9610  cnfcom  9621  rankr1ai  9722  rankonidlem  9752  rankxplim2  9804  oncard  9884  ficardom  9885  cardne  9889  acnnum  9974  alephord2i  9999  cardaleph  10011  aceq3lem  10042  dfac5lem5  10049  dfac12lem3  10068  ackbij1lem16  10156  cfslb  10188  cfslb2n  10190  cfsmolem  10192  fin4i  10220  infpssr  10230  fin1a2lem6  10327  axdc3lem2  10373  axcclem  10379  ttukeylem6  10436  fodomb  10448  gchi  10547  pwfseq  10587  inawina  10613  wunfi  10644  inar1  10698  ltexnq  10898  ltbtwnnq  10901  ltexprlem4  10962  ltexpri  10966  prlem936  10970  suplem1pr  10975  suplem2pr  10976  recexsrlem  11026  mulgt0sr  11028  map2psrpr  11033  supsr  11035  eqlei  11256  eqlei2  11257  ledivp1i  12081  nnind  12192  nnmulcl  12198  nn0ge2m1nn  12507  nnnegz  12527  ublbneg  12883  xmulasslem  13237  ixxssixx  13312  iccshftri  13440  iccshftli  13442  iccdili  13444  icccntri  13446  elfz1b  13547  fzo1fzo0n0  13670  elfzonlteqm1  13696  elfzo0l  13711  ssfzo12  13714  fzoopth  13717  elfzo1elm1fzo0  13723  elfzr  13736  elfzlmr  13737  zmodidfzoimp  13860  mptnn0fsuppr  13961  seqp1  13978  seqcl2  13982  seqfveq2  13986  seqshft2  13990  monoord  13994  seqsplit  13997  seqcaopr3  13999  seqf1olem2a  14002  seqf1o  14005  seqid2  14010  seqhomo  14011  hashf1rn  14314  hashinfxadd  14347  hashf1lem2  14418  seqcoll  14426  hash2pr  14431  pr2pwpr  14441  hashge2el2difr  14443  hash3tr  14453  fi1uzind  14469  brfi1indALT  14472  elovmptnn0wrd  14521  swrdswrd  14667  pfxccatin12lem2a  14689  swrdccat  14697  swrdccatin1d  14705  swrdccatin2d  14706  repswccat  14748  cshwidxmod  14765  relexpsucnnr  14987  rtrclreclem3  15022  rtrclreclem4  15023  dfrtrcl2  15024  relexpindlem  15025  relexpind  15026  rtrclind  15027  cjre  15101  climeu  15517  climub  15624  fsum2d  15733  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  prodfn0  15859  prodfrec  15860  ntrivcvg  15862  fprodabs  15939  fprod2d  15946  fprodefsum  16060  ruclem9  16205  dvdsmod0  16227  p1modz1  16228  dvdsmodexp  16229  dvdsabseq  16282  mod2eq1n2dvds  16316  mulsucdiv2z  16322  nno  16351  nn0o  16352  sadcadd  16427  sadadd2  16429  saddisjlem  16433  smuval2  16451  smupval  16457  smueqlem  16459  smumullem  16461  dfgcd2  16515  lcmgcdlem  16575  lcmftp  16605  exprmfct  16674  eulerthlem2  16752  dvdsprmpweqnn  16856  dvdsprmpweqle  16857  pcmpt  16863  vdwlem10  16961  cshwsidrepsw  17064  cshwshashlem1  17066  prmlem1a  17077  setsn0fun  17143  ressval3d  17216  mreexexd  17614  letsr  18559  insubm  18786  ghmghmrn  19210  pmtrfrn  19433  pmtr3ncom  19450  gsmtrcl  19491  psgnsn  19495  sylow1lem1  19573  efginvrel2  19702  efgsrel  19709  cntzcmnss  19816  gsum2dlem2  19946  telgsumfzs  19964  dprdval  19980  ablfac1eulem  20049  pgpfac1  20057  pgpfac  20061  srgpcomp  20199  ringrng  20266  ring1ne0  20280  rngimf1o  20434  rngimrnghm  20435  rngimcnv  20436  0ringnnzr  20502  zrhpsgnelbas  21574  psgndiflemA  21581  mplcoe1  22015  mplcoe3  22016  mplcoe5lem  22017  mplcoe5  22018  mpfaddcl  22091  mpfmulcl  22092  coe1ae0  22180  coe1fzgsumd  22269  gsummoncoe1  22273  pf1addcl  22318  pf1mulcl  22319  evl1gsumd  22322  mamufacex  22361  mat0dimcrng  22435  mavmulsolcl  22516  mdetunilem9  22585  cramerlem3  22654  pmatcollpw3fi1  22753  pm2mpfo  22779  chmaidscmat  22813  chfacfscmul0  22823  chfacfpmmul0  22827  cpmadugsumlemF  22841  tg2  22930  neindisj2  23088  neiptopnei  23097  t1t0  23313  fiuncmp  23369  hmeof1o  23729  ist1-5lem  23785  t1r0  23786  alexsublem  24009  imasdsf1olem  24338  tgioo  24761  fsumcn  24837  voliunlem3  25519  itgfsum  25794  dvbsss  25869  dvmptfsum  25942  dvfsumlem2  25994  dvfsumlem4  25996  plyco  26206  dgrcolem1  26238  dgrco  26240  dvntaylp  26336  taylthlem1  26338  jensen  26952  bposlem5  27251  lgsqrmodndvds  27316  gausslemma2dlem0i  27327  gausslemma2dlem4  27332  lgsquad2lem2  27348  2lgslem3  27367  2lgs  27370  2lgsoddprm  27379  dchrisum0flb  27473  pntpbnd1  27549  pntlemf  27568  madebdayim  27880  oldbdayim  27881  pw2cut  28452  brbtwn  28968  brcgr  28969  umgrnloopv  29175  umgrnloop  29177  usgrnloopvALT  29270  usgrnloopALT  29272  usgredg2vlem2  29295  subgrprop  29342  uvtxnbgrvtx  29462  cusgrsize2inds  29522  rgrprop  29629  rusgrprop  29631  wlkprop  29680  wlkvtxeledg  29692  wlkeq  29702  wlkl1loop  29706  wlk1walk  29707  uspgr2wlkeqi  29716  wlkreslem  29736  wlkres  29737  redwlk  29739  lfgrwlknloop  29756  2pthnloop  29799  usgr2trlncl  29828  usgr2pth  29832  clwlkcompim  29848  clwlkcompbp  29850  uspgrn2crct  29876  crctcshwlkn0  29889  wwlknp  29911  wwlkswwlksn  29933  wlkiswwlks2lem4  29940  wlkiswwlks2  29943  wlklnwwlkln2lem  29950  wwlksnext  29961  wwlksnextbi  29962  wwlksnredwwlkn0  29964  wwlksnextwrd  29965  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlkflem  30074  clwwisshclwws  30085  clwwlknp  30107  clwwlknwwlksn  30108  clwwlkwwlksb  30124  clwwlkext2edg  30126  umgrhashecclwwlk  30148  clwwlknun  30182  1pthond  30214  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eupth2  30309  3vfriswmgr  30348  3cyclfrgrrn1  30355  n4cyclfrgr  30361  frgrnbnb  30363  frgrncvvdeqlem3  30371  frgrncvvdeqlem6  30374  frgrncvvdeqlem7  30375  frgrncvvdeqlem8  30376  frgrwopreglem4a  30380  frgrwopreg  30393  frgrregorufr0  30394  frgr2wwlkeqm  30401  2clwwlk2clwwlklem  30416  wlkl0  30437  frgrreggt1  30463  frgrregord013  30465  frgrregord13  30466  frgrogt3nreg  30467  friendshipgt3  30468  friendship  30469  blocn2  30879  cvexchlem  32439  cdj3lem2b  32508  nnindf  32893  gsumwun  33137  domnprodn0  33336  issgon  34267  sitgclg  34486  sseqp1  34539  bnj938  35079  bnj964  35085  bnj1052  35117  bnj1125  35134  onvf1odlem4  35288  subfacp1lem6  35367  cvmliftlem7  35473  cvmliftlem10  35476  mclsrcl  35743  pprodss4v  36064  segleantisym  36297  rankeq1o  36353  bj-restv  37407  iooelexlt  37678  relowlssretop  37679  rdgeqoa  37686  matunitlindflem1  37937  poimirlem22  37963  poimirlem25  37966  poimirlem28  37969  poimirlem31  37972  mblfinlem3  37980  mbfresfi  37987  mettrifi  38078  opidon2OLD  38175  isexid2  38176  grpomndo  38196  elghomlem2OLD  38207  rngoidmlem  38257  rngoueqz  38261  iscringd  38319  cdlemk35s  41383  cdlemk39s  41385  cdlemk42  41387  uzindd  42417  mzpadd  43170  mzpmul  43171  mzpcompact2  43184  dford3lem2  43455  aomclem6  43487  cnsrexpcl  43593  ensucne0OLD  43957  pr2cv  43975  relexpss1d  44132  iunrelexpmin1  44135  iunrelexpmin2  44139  tfindsd  44637  nzin  44745  axc11next  44833  iotavalsb  44860  ssdec  45518  fperiodmullem  45736  monoordxrv  45909  fmul01  46010  fmulcl  46011  fmuldfeqlem1  46012  fmuldfeq  46013  iblspltprt  46401  itgspltprt  46407  stoweidlem2  46430  stoweidlem3  46431  stoweidlem6  46434  stoweidlem8  46436  stoweidlem17  46445  stoweidlem19  46447  stoweidlem21  46449  stoweidlem26  46454  stoweidlem31  46459  stoweidlem43  46471  fourierdlem42  46577  funressnfv  47491  eu2ndop1stv  47573  afv0fv0  47597  afv0nbfvbi  47599  funressnbrafv2  47692  funbrafv2  47695  nelbrim  47723  ssfz12  47762  smonoord  47825  iccpartiltu  47882  iccpartigtl  47883  iccelpart  47893  icceuelpart  47896  fargshiftf  47900  fargshiftf1  47901  fargshiftfo  47902  sprel  47944  sprsymrelf1lem  47951  sprsymrelfolem2  47953  prproropf1olem4  47966  lighneallem4  48073  mogoldbblem  48196  fpprnn  48206  fpprwppr  48215  fpprwpprb  48216  sbgoldbwt  48253  bgoldbtbndlem2  48282  bgoldbtbndlem4  48284  tgoldbach  48293  grimprop  48359  grlimprop  48460  grilcbri2  48487  upwlkwlk  48615  clcllaw  48667  intop  48679  clintop  48684  assintop  48685  assintopcllaw  48688  lmod0rng  48705  ztprmneprm  48823  scmsuppss  48847  ply1mulgsumlem1  48862  ply1mulgsumlem2  48863  lcoel0  48904  ellcoellss  48911  lindslinindsimp2lem5  48938  ldepspr  48949  flnn0div2ge  49009  nnolog2flm1  49066  blengt1fldiv2p1  49069  dignn0flhalf  49094  naryfvalelfv  49108  0aryfvalelfv  49111  fv1arycl  49113  fv2arycl  49124