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  2437  mo4  2567  sbcn1  3774  sbcim1  3775  sbcim1OLD  3776  sbcbi1  3781  sbcel21v  3793  csbie2df  4379  elimasni  5996  sotri  6029  unixpid  6184  f0rn0  6655  f1ocnv  6724  funbrfv  6814  elfvmptrab1w  6895  f1dom3el3dif  7136  oprabidw  7299  oprabid  7300  oprabv  7326  ndmovordi  7454  elovmporab  7506  elovmporab1w  7507  elovmporab1  7508  elovmpt3rab1  7520  limomss  7705  unielxp  7855  bropfvvvvlem  7915  f1o2ndf1  7947  smogt  8182  tfrlem1  8191  oawordeulem  8361  omass  8387  ecopovtrn  8583  mapfvd  8641  findcard2d  8914  ssfi  8921  f1domfi  8932  php  8957  phpOLD  8970  unxpdom  8991  findcard3  9018  isfinite2  9033  fsuppimp  9095  fsuppunfi  9109  fsuppunbi  9110  fsuppres  9114  infsupprpr  9224  cantnfval2  9388  cantnfle  9390  cantnfp1lem3  9399  cantnflem1  9408  cnfcom  9419  rankr1ai  9540  rankonidlem  9570  rankxplim2  9622  oncard  9702  ficardom  9703  cardne  9707  acnnum  9792  alephord2i  9817  cardaleph  9829  aceq3lem  9860  dfac5lem5  9867  dfac12lem3  9885  ackbij1lem16  9975  cfslb  10006  cfslb2n  10008  cfsmolem  10010  fin4i  10038  infpssr  10048  fin1a2lem6  10145  axdc3lem2  10191  axcclem  10197  ttukeylem6  10254  fodomb  10266  gchi  10364  fpwwe2lem4  10374  pwfseqlem4  10402  pwfseq  10404  inawina  10430  wunfi  10461  inar1  10515  ltexnq  10715  ltbtwnnq  10718  ltexprlem4  10779  ltexpri  10783  prlem936  10787  suplem1pr  10792  suplem2pr  10793  recexsrlem  10843  mulgt0sr  10845  map2psrpr  10850  supsr  10852  eqlei  11068  eqlei2  11069  ledivp1i  11883  nnind  11974  nnmulcl  11980  nn0ge2m1nn  12285  nnnegz  12305  ublbneg  12655  xmulasslem  13001  ixxssixx  13075  iccshftri  13201  iccshftli  13203  iccdili  13205  icccntri  13207  elfz1b  13307  fzo1fzo0n0  13419  elfzonlteqm1  13444  elfzo0l  13458  ssfzo12  13461  elfzo1elm1fzo0  13469  elfzr  13481  elfzlmr  13482  zmodidfzoimp  13602  mptnn0fsuppr  13700  seqp1  13717  seqcl2  13722  seqfveq2  13726  seqshft2  13730  monoord  13734  seqsplit  13737  seqcaopr3  13739  seqf1olem2a  13742  seqf1o  13745  seqid2  13750  seqhomo  13751  hashf1rn  14048  hashinfxadd  14081  hashf1lem2  14151  seqcoll  14159  hash2pr  14164  pr2pwpr  14174  hashge2el2difr  14176  hash3tr  14185  fi1uzind  14192  brfi1indALT  14195  elovmptnn0wrd  14243  swrdswrd  14399  pfxccatin12lem2a  14421  swrdccat  14429  swrdccatin1d  14437  swrdccatin2d  14438  repswccat  14480  cshwidxmod  14497  relexpsucnnr  14717  rtrclreclem3  14752  rtrclreclem4  14753  dfrtrcl2  14754  relexpindlem  14755  relexpind  14756  rtrclind  14757  cjre  14831  climeu  15245  climub  15354  fsum2d  15464  fsumabs  15494  fsumrlim  15504  fsumo1  15505  fsumiun  15514  prodfn0  15587  prodfrec  15588  ntrivcvg  15590  fprodabs  15665  fprod2d  15672  fprodefsum  15785  ruclem9  15928  dvdsmod0  15950  p1modz1  15951  dvdsmodexp  15952  dvdsabseq  16003  mod2eq1n2dvds  16037  mulsucdiv2z  16043  nno  16072  nn0o  16073  sadcadd  16146  sadadd2  16148  saddisjlem  16152  smuval2  16170  smupval  16176  smueqlem  16178  smumullem  16180  dfgcd2  16235  lcmgcdlem  16292  lcmftp  16322  exprmfct  16390  eulerthlem2  16464  dvdsprmpweqnn  16567  dvdsprmpweqle  16568  pcmpt  16574  vdwlem10  16672  cshwsidrepsw  16776  cshwshashlem1  16778  prmlem1a  16789  setsn0fun  16855  ressval3d  16937  ressval3dOLD  16938  mreexexd  17338  letsr  18292  insubm  18438  ghmghmrn  18834  pmtrfrn  19047  pmtr3ncom  19064  gsmtrcl  19105  psgnsn  19109  sylow1lem1  19184  efginvrel2  19314  efgsrel  19321  cntzcmnss  19423  gsum2dlem2  19553  telgsumfzs  19571  dprdval  19587  ablfac1eulem  19656  pgpfac1  19664  pgpfac  19668  srgpcomp  19749  ring1ne0  19811  rimf1o  19959  rimrhm  19960  brric2  19970  0ringnnzr  20521  zrhpsgnelbas  20780  psgndiflemA  20787  mplcoe1  21219  mplcoe3  21220  mplcoe5lem  21221  mplcoe5  21222  mpfaddcl  21296  mpfmulcl  21297  coe1ae0  21368  coe1fzgsumd  21454  gsummoncoe1  21456  pf1addcl  21500  pf1mulcl  21501  evl1gsumd  21504  mamufacex  21519  mat0dimcrng  21600  mavmulsolcl  21681  mdetunilem9  21750  cramerlem3  21819  pmatcollpw3fi1  21918  pm2mpfo  21944  chmaidscmat  21978  chfacfscmul0  21988  chfacfpmmul0  21992  cpmadugsumlemF  22006  tg2  22096  neindisj2  22255  neiptopnei  22264  t1t0  22480  fiuncmp  22536  hmeof1o  22896  ist1-5lem  22952  t1r0  22953  alexsublem  23176  imasdsf1olem  23507  tgioo  23940  fsumcn  24014  voliunlem3  24697  itgfsum  24972  dvbsss  25047  dvmptfsum  25120  dvfsumlem2  25172  dvfsumlem4  25174  plyco  25383  dgrcolem1  25415  dgrco  25417  dvntaylp  25511  taylthlem1  25513  jensen  26119  bposlem5  26417  lgsqrmodndvds  26482  gausslemma2dlem0i  26493  gausslemma2dlem4  26498  lgsquad2lem2  26514  2lgslem3  26533  2lgs  26536  2lgsoddprm  26545  dchrisum0flb  26639  pntpbnd1  26715  pntlemf  26734  brbtwn  27248  brcgr  27249  umgrnloopv  27457  umgrnloop  27459  usgrnloopvALT  27549  usgrnloopALT  27551  usgredg2vlem2  27574  subgrprop  27621  uvtxnbgrvtx  27741  cusgrsize2inds  27801  rgrprop  27908  rusgrprop  27910  wlkprop  27959  wlkvtxeledg  27971  wlkeq  27981  wlkl1loop  27985  wlk1walk  27986  uspgr2wlkeqi  27995  wlkreslem  28017  wlkres  28018  redwlk  28020  lfgrwlknloop  28037  2pthnloop  28078  usgr2trlncl  28107  usgr2pth  28111  clwlkcompim  28127  clwlkcompbp  28129  uspgrn2crct  28152  crctcshwlkn0  28165  wwlknp  28187  wwlkswwlksn  28209  wlkiswwlks2lem4  28216  wlkiswwlks2  28219  wlklnwwlkln2lem  28226  wwlksnext  28237  wwlksnextbi  28238  wwlksnredwwlkn0  28240  wwlksnextwrd  28241  clwlkclwwlklem2a  28341  clwlkclwwlklem2  28343  clwlkclwwlkflem  28347  clwwisshclwws  28358  clwwlknp  28380  clwwlknwwlksn  28381  clwwlkwwlksb  28397  clwwlkext2edg  28399  umgrhashecclwwlk  28421  clwwlknun  28455  1pthond  28487  upgr3v3e3cycl  28523  upgr4cycl4dv4e  28528  eupth2  28582  3vfriswmgr  28621  3cyclfrgrrn1  28628  n4cyclfrgr  28634  frgrnbnb  28636  frgrncvvdeqlem3  28644  frgrncvvdeqlem6  28647  frgrncvvdeqlem7  28648  frgrncvvdeqlem8  28649  frgrwopreglem4a  28653  frgrwopreg  28666  frgrregorufr0  28667  frgr2wwlkeqm  28674  2clwwlk2clwwlklem  28689  wlkl0  28710  frgrreggt1  28736  frgrregord013  28738  frgrregord13  28739  frgrogt3nreg  28740  friendshipgt3  28741  friendship  28742  blocn2  29149  cvexchlem  30709  cdj3lem2b  30778  cnvoprabOLD  31034  nnindf  31112  issgon  32070  sitgclg  32288  sseqp1  32341  bnj938  32896  bnj964  32902  bnj1052  32934  bnj1125  32951  subfacp1lem6  33126  cvmliftlem7  33232  cvmliftlem10  33235  mclsrcl  33502  madebdayim  34049  oldbdayim  34050  pprodss4v  34165  segleantisym  34396  rankeq1o  34452  bj-restv  35245  iooelexlt  35512  relowlssretop  35513  rdgeqoa  35520  matunitlindflem1  35752  poimirlem22  35778  poimirlem25  35781  poimirlem28  35784  poimirlem31  35787  mblfinlem3  35795  mbfresfi  35802  mettrifi  35894  opidon2OLD  35991  isexid2  35992  grpomndo  36012  elghomlem2OLD  36023  rngoidmlem  36073  rngoueqz  36077  iscringd  36135  cdlemk35s  38930  cdlemk39s  38932  cdlemk42  38934  uzindd  39965  mzpadd  40540  mzpmul  40541  mzpcompact2  40554  dford3lem2  40829  aomclem6  40864  cnsrexpcl  40970  ensucne0OLD  41099  pr2cv  41108  relexpss1d  41266  iunrelexpmin1  41269  iunrelexpmin2  41273  tfindsd  41776  nzin  41889  axc11next  41977  iotavalsb  42004  ssdec  42591  fperiodmullem  42796  monoordxrv  42976  fmul01  43075  fmulcl  43076  fmuldfeqlem1  43077  fmuldfeq  43078  fprodcnlem  43094  iblspltprt  43468  itgspltprt  43474  stoweidlem2  43497  stoweidlem3  43498  stoweidlem6  43501  stoweidlem8  43503  stoweidlem17  43512  stoweidlem19  43514  stoweidlem21  43516  stoweidlem26  43521  stoweidlem31  43526  stoweidlem43  43538  fourierdlem42  43644  funressnfv  44488  eu2ndop1stv  44568  afv0fv0  44592  afv0nbfvbi  44594  funressnbrafv2  44687  funbrafv2  44690  nelbrim  44718  ssfz12  44758  fzoopth  44771  smonoord  44775  iccpartiltu  44826  iccpartigtl  44827  iccelpart  44837  icceuelpart  44840  fargshiftf  44844  fargshiftf1  44845  fargshiftfo  44846  sprel  44888  sprsymrelf1lem  44895  sprsymrelfolem2  44897  prproropf1olem4  44910  lighneallem4  45014  mogoldbblem  45124  fpprnn  45134  fpprwppr  45143  fpprwpprb  45144  sbgoldbwt  45181  bgoldbtbndlem2  45210  bgoldbtbndlem4  45212  tgoldbach  45221  upwlkwlk  45253  clcllaw  45337  intop  45349  clintop  45354  assintop  45355  assintopcllaw  45358  lmod0rng  45378  ringrng  45389  rngimf1o  45415  rngimrnghm  45416  ztprmneprm  45635  scmsuppss  45660  ply1mulgsumlem1  45679  ply1mulgsumlem2  45680  lcoel0  45721  ellcoellss  45728  lindslinindsimp2lem5  45755  ldepspr  45766  flnn0div2ge  45831  nnolog2flm1  45888  blengt1fldiv2p1  45891  dignn0flhalf  45916  naryfvalelfv  45930  0aryfvalelfv  45933  fv1arycl  45935  fv2arycl  45946