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  2434  mo4  2559  sbcn1  3797  sbcim1  3798  sbcbi1  3802  sbcel21v  3812  sbccomlem  3823  csbie2df  4396  elimasni  6046  sotri  6080  unixpid  6236  f0rn0  6713  f1ocnv  6780  funbrfv  6875  elfvmptrab1w  6961  f1dom3el3dif  7210  oprabidw  7384  oprabid  7385  oprabv  7413  ndmovordi  7544  elovmporab  7599  elovmporab1w  7600  elovmporab1  7601  elovmpt3rab1  7613  limomss  7811  unielxp  7969  bropfvvvvlem  8031  f1o2ndf1  8062  smogt  8297  tfrlem1  8305  oawordeulem  8479  omass  8505  ecopovtrn  8754  mapfvd  8813  findcard2d  9090  ssfi  9097  f1domfi  9105  php  9131  unxpdom  9158  findcard3  9187  findcard3OLD  9188  isfinite2  9203  fsuppimp  9277  fsuppunfi  9297  fsuppunbi  9298  fsuppres  9302  infsupprpr  9415  cantnfval2  9584  cantnfle  9586  cantnfp1lem3  9595  cantnflem1  9604  cnfcom  9615  rankr1ai  9713  rankonidlem  9743  rankxplim2  9795  oncard  9875  ficardom  9876  cardne  9880  acnnum  9965  alephord2i  9990  cardaleph  10002  aceq3lem  10033  dfac5lem5  10040  dfac12lem3  10059  ackbij1lem16  10147  cfslb  10179  cfslb2n  10181  cfsmolem  10183  fin4i  10211  infpssr  10221  fin1a2lem6  10318  axdc3lem2  10364  axcclem  10370  ttukeylem6  10427  fodomb  10439  gchi  10537  pwfseq  10577  inawina  10603  wunfi  10634  inar1  10688  ltexnq  10888  ltbtwnnq  10891  ltexprlem4  10952  ltexpri  10956  prlem936  10960  suplem1pr  10965  suplem2pr  10966  recexsrlem  11016  mulgt0sr  11018  map2psrpr  11023  supsr  11025  eqlei  11244  eqlei2  11245  ledivp1i  12068  nnind  12164  nnmulcl  12170  nn0ge2m1nn  12472  nnnegz  12492  ublbneg  12852  xmulasslem  13205  ixxssixx  13280  iccshftri  13408  iccshftli  13410  iccdili  13412  icccntri  13414  elfz1b  13514  fzo1fzo0n0  13636  elfzonlteqm1  13662  elfzo0l  13677  ssfzo12  13680  fzoopth  13683  elfzo1elm1fzo0  13689  elfzr  13701  elfzlmr  13702  zmodidfzoimp  13823  mptnn0fsuppr  13924  seqp1  13941  seqcl2  13945  seqfveq2  13949  seqshft2  13953  monoord  13957  seqsplit  13960  seqcaopr3  13962  seqf1olem2a  13965  seqf1o  13968  seqid2  13973  seqhomo  13974  hashf1rn  14277  hashinfxadd  14310  hashf1lem2  14381  seqcoll  14389  hash2pr  14394  pr2pwpr  14404  hashge2el2difr  14406  hash3tr  14416  fi1uzind  14432  brfi1indALT  14435  elovmptnn0wrd  14484  swrdswrd  14629  pfxccatin12lem2a  14651  swrdccat  14659  swrdccatin1d  14667  swrdccatin2d  14668  repswccat  14710  cshwidxmod  14727  relexpsucnnr  14950  rtrclreclem3  14985  rtrclreclem4  14986  dfrtrcl2  14987  relexpindlem  14988  relexpind  14989  rtrclind  14990  cjre  15064  climeu  15480  climub  15587  fsum2d  15696  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  prodfn0  15819  prodfrec  15820  ntrivcvg  15822  fprodabs  15899  fprod2d  15906  fprodefsum  16020  ruclem9  16165  dvdsmod0  16187  p1modz1  16188  dvdsmodexp  16189  dvdsabseq  16242  mod2eq1n2dvds  16276  mulsucdiv2z  16282  nno  16311  nn0o  16312  sadcadd  16387  sadadd2  16389  saddisjlem  16393  smuval2  16411  smupval  16417  smueqlem  16419  smumullem  16421  dfgcd2  16475  lcmgcdlem  16535  lcmftp  16565  exprmfct  16633  eulerthlem2  16711  dvdsprmpweqnn  16815  dvdsprmpweqle  16816  pcmpt  16822  vdwlem10  16920  cshwsidrepsw  17023  cshwshashlem1  17025  prmlem1a  17036  setsn0fun  17102  ressval3d  17175  mreexexd  17572  letsr  18517  insubm  18710  ghmghmrn  19132  pmtrfrn  19355  pmtr3ncom  19372  gsmtrcl  19413  psgnsn  19417  sylow1lem1  19495  efginvrel2  19624  efgsrel  19631  cntzcmnss  19738  gsum2dlem2  19868  telgsumfzs  19886  dprdval  19902  ablfac1eulem  19971  pgpfac1  19979  pgpfac  19983  srgpcomp  20121  ringrng  20188  ring1ne0  20202  rngimf1o  20357  rngimrnghm  20358  rngimcnv  20359  0ringnnzr  20428  zrhpsgnelbas  21519  psgndiflemA  21526  mplcoe1  21960  mplcoe3  21961  mplcoe5lem  21962  mplcoe5  21963  mpfaddcl  22028  mpfmulcl  22029  coe1ae0  22117  coe1fzgsumd  22207  gsummoncoe1  22211  pf1addcl  22256  pf1mulcl  22257  evl1gsumd  22260  mamufacex  22299  mat0dimcrng  22373  mavmulsolcl  22454  mdetunilem9  22523  cramerlem3  22592  pmatcollpw3fi1  22691  pm2mpfo  22717  chmaidscmat  22751  chfacfscmul0  22761  chfacfpmmul0  22765  cpmadugsumlemF  22779  tg2  22868  neindisj2  23026  neiptopnei  23035  t1t0  23251  fiuncmp  23307  hmeof1o  23667  ist1-5lem  23723  t1r0  23724  alexsublem  23947  imasdsf1olem  24277  tgioo  24700  fsumcn  24777  voliunlem3  25469  itgfsum  25744  dvbsss  25819  dvmptfsum  25895  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem4  25952  plyco  26162  dgrcolem1  26195  dgrco  26197  dvntaylp  26295  taylthlem1  26297  jensen  26915  bposlem5  27215  lgsqrmodndvds  27280  gausslemma2dlem0i  27291  gausslemma2dlem4  27296  lgsquad2lem2  27312  2lgslem3  27331  2lgs  27334  2lgsoddprm  27343  dchrisum0flb  27437  pntpbnd1  27513  pntlemf  27532  madebdayim  27820  oldbdayim  27821  pw2cut  28366  brbtwn  28862  brcgr  28863  umgrnloopv  29069  umgrnloop  29071  usgrnloopvALT  29164  usgrnloopALT  29166  usgredg2vlem2  29189  subgrprop  29236  uvtxnbgrvtx  29356  cusgrsize2inds  29417  rgrprop  29524  rusgrprop  29526  wlkprop  29575  wlkvtxeledg  29587  wlkeq  29597  wlkl1loop  29601  wlk1walk  29602  uspgr2wlkeqi  29611  wlkreslem  29631  wlkres  29632  redwlk  29634  lfgrwlknloop  29651  2pthnloop  29694  usgr2trlncl  29723  usgr2pth  29727  clwlkcompim  29743  clwlkcompbp  29745  uspgrn2crct  29771  crctcshwlkn0  29784  wwlknp  29806  wwlkswwlksn  29828  wlkiswwlks2lem4  29835  wlkiswwlks2  29838  wlklnwwlkln2lem  29845  wwlksnext  29856  wwlksnextbi  29857  wwlksnredwwlkn0  29859  wwlksnextwrd  29860  clwlkclwwlklem2a  29960  clwlkclwwlklem2  29962  clwlkclwwlkflem  29966  clwwisshclwws  29977  clwwlknp  29999  clwwlknwwlksn  30000  clwwlkwwlksb  30016  clwwlkext2edg  30018  umgrhashecclwwlk  30040  clwwlknun  30074  1pthond  30106  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eupth2  30201  3vfriswmgr  30240  3cyclfrgrrn1  30247  n4cyclfrgr  30253  frgrnbnb  30255  frgrncvvdeqlem3  30263  frgrncvvdeqlem6  30266  frgrncvvdeqlem7  30267  frgrncvvdeqlem8  30268  frgrwopreglem4a  30272  frgrwopreg  30285  frgrregorufr0  30286  frgr2wwlkeqm  30293  2clwwlk2clwwlklem  30308  wlkl0  30329  frgrreggt1  30355  frgrregord013  30357  frgrregord13  30358  frgrogt3nreg  30359  friendshipgt3  30360  friendship  30361  blocn2  30770  cvexchlem  32330  cdj3lem2b  32399  nnindf  32777  gsumwun  33031  domnprodn0  33225  issgon  34089  sitgclg  34309  sseqp1  34362  bnj938  34903  bnj964  34909  bnj1052  34941  bnj1125  34958  onvf1odlem4  35078  subfacp1lem6  35157  cvmliftlem7  35263  cvmliftlem10  35266  mclsrcl  35533  pprodss4v  35857  segleantisym  36088  rankeq1o  36144  bj-restv  37068  iooelexlt  37335  relowlssretop  37336  rdgeqoa  37343  matunitlindflem1  37595  poimirlem22  37621  poimirlem25  37624  poimirlem28  37627  poimirlem31  37630  mblfinlem3  37638  mbfresfi  37645  mettrifi  37736  opidon2OLD  37833  isexid2  37834  grpomndo  37854  elghomlem2OLD  37865  rngoidmlem  37915  rngoueqz  37919  iscringd  37977  cdlemk35s  40916  cdlemk39s  40918  cdlemk42  40920  uzindd  41950  mzpadd  42711  mzpmul  42712  mzpcompact2  42725  dford3lem2  43000  aomclem6  43032  cnsrexpcl  43138  ensucne0OLD  43503  pr2cv  43521  relexpss1d  43678  iunrelexpmin1  43681  iunrelexpmin2  43685  tfindsd  44183  nzin  44291  axc11next  44379  iotavalsb  44406  ssdec  45066  fperiodmullem  45285  monoordxrv  45461  fmul01  45562  fmulcl  45563  fmuldfeqlem1  45564  fmuldfeq  45565  iblspltprt  45955  itgspltprt  45961  stoweidlem2  45984  stoweidlem3  45985  stoweidlem6  45988  stoweidlem8  45990  stoweidlem17  45999  stoweidlem19  46001  stoweidlem21  46003  stoweidlem26  46008  stoweidlem31  46013  stoweidlem43  46025  fourierdlem42  46131  funressnfv  47028  eu2ndop1stv  47110  afv0fv0  47134  afv0nbfvbi  47136  funressnbrafv2  47229  funbrafv2  47232  nelbrim  47260  ssfz12  47299  smonoord  47356  iccpartiltu  47407  iccpartigtl  47408  iccelpart  47418  icceuelpart  47421  fargshiftf  47425  fargshiftf1  47426  fargshiftfo  47427  sprel  47469  sprsymrelf1lem  47476  sprsymrelfolem2  47478  prproropf1olem4  47491  lighneallem4  47595  mogoldbblem  47705  fpprnn  47715  fpprwppr  47724  fpprwpprb  47725  sbgoldbwt  47762  bgoldbtbndlem2  47791  bgoldbtbndlem4  47793  tgoldbach  47802  grimprop  47868  grlimprop  47969  grilcbri2  47996  upwlkwlk  48124  clcllaw  48176  intop  48188  clintop  48193  assintop  48194  assintopcllaw  48197  lmod0rng  48214  ztprmneprm  48332  scmsuppss  48356  ply1mulgsumlem1  48372  ply1mulgsumlem2  48373  lcoel0  48414  ellcoellss  48421  lindslinindsimp2lem5  48448  ldepspr  48459  flnn0div2ge  48519  nnolog2flm1  48576  blengt1fldiv2p1  48579  dignn0flhalf  48604  naryfvalelfv  48618  0aryfvalelfv  48621  fv1arycl  48623  fv2arycl  48634