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  667  axc16i  2434  mo4  2564  sbcn1  3776  sbcim1  3777  sbcim1OLD  3778  sbcbi1  3782  sbcel21v  3794  csbie2df  4380  elimasni  6009  sotri  6047  unixpid  6202  f0rn0  6689  f1ocnv  6758  funbrfv  6852  elfvmptrab1w  6933  f1dom3el3dif  7174  oprabidw  7338  oprabid  7339  oprabv  7367  ndmovordi  7495  elovmporab  7547  elovmporab1w  7548  elovmporab1  7549  elovmpt3rab1  7561  limomss  7749  unielxp  7901  bropfvvvvlem  7963  f1o2ndf1  7994  smogt  8229  tfrlem1  8238  oawordeulem  8416  omass  8442  ecopovtrn  8640  mapfvd  8698  findcard2d  8987  ssfi  8994  f1domfi  9005  php  9031  phpOLD  9043  unxpdom  9074  findcard3  9101  isfinite2  9116  fsuppimp  9178  fsuppunfi  9192  fsuppunbi  9193  fsuppres  9197  infsupprpr  9307  cantnfval2  9471  cantnfle  9473  cantnfp1lem3  9482  cantnflem1  9491  cnfcom  9502  rankr1ai  9600  rankonidlem  9630  rankxplim2  9682  oncard  9762  ficardom  9763  cardne  9767  acnnum  9854  alephord2i  9879  cardaleph  9891  aceq3lem  9922  dfac5lem5  9929  dfac12lem3  9947  ackbij1lem16  10037  cfslb  10068  cfslb2n  10070  cfsmolem  10072  fin4i  10100  infpssr  10110  fin1a2lem6  10207  axdc3lem2  10253  axcclem  10259  ttukeylem6  10316  fodomb  10328  gchi  10426  fpwwe2lem4  10436  pwfseqlem4  10464  pwfseq  10466  inawina  10492  wunfi  10523  inar1  10577  ltexnq  10777  ltbtwnnq  10780  ltexprlem4  10841  ltexpri  10845  prlem936  10849  suplem1pr  10854  suplem2pr  10855  recexsrlem  10905  mulgt0sr  10907  map2psrpr  10912  supsr  10914  eqlei  11131  eqlei2  11132  ledivp1i  11946  nnind  12037  nnmulcl  12043  nn0ge2m1nn  12348  nnnegz  12368  ublbneg  12719  xmulasslem  13065  ixxssixx  13139  iccshftri  13265  iccshftli  13267  iccdili  13269  icccntri  13271  elfz1b  13371  fzo1fzo0n0  13484  elfzonlteqm1  13509  elfzo0l  13523  ssfzo12  13526  elfzo1elm1fzo0  13534  elfzr  13546  elfzlmr  13547  zmodidfzoimp  13667  mptnn0fsuppr  13765  seqp1  13782  seqcl2  13787  seqfveq2  13791  seqshft2  13795  monoord  13799  seqsplit  13802  seqcaopr3  13804  seqf1olem2a  13807  seqf1o  13810  seqid2  13815  seqhomo  13816  hashf1rn  14112  hashinfxadd  14145  hashf1lem2  14215  seqcoll  14223  hash2pr  14228  pr2pwpr  14238  hashge2el2difr  14240  hash3tr  14249  fi1uzind  14256  brfi1indALT  14259  elovmptnn0wrd  14307  swrdswrd  14463  pfxccatin12lem2a  14485  swrdccat  14493  swrdccatin1d  14501  swrdccatin2d  14502  repswccat  14544  cshwidxmod  14561  relexpsucnnr  14781  rtrclreclem3  14816  rtrclreclem4  14817  dfrtrcl2  14818  relexpindlem  14819  relexpind  14820  rtrclind  14821  cjre  14895  climeu  15309  climub  15418  fsum2d  15528  fsumabs  15558  fsumrlim  15568  fsumo1  15569  fsumiun  15578  prodfn0  15651  prodfrec  15652  ntrivcvg  15654  fprodabs  15729  fprod2d  15736  fprodefsum  15849  ruclem9  15992  dvdsmod0  16014  p1modz1  16015  dvdsmodexp  16016  dvdsabseq  16067  mod2eq1n2dvds  16101  mulsucdiv2z  16107  nno  16136  nn0o  16137  sadcadd  16210  sadadd2  16212  saddisjlem  16216  smuval2  16234  smupval  16240  smueqlem  16242  smumullem  16244  dfgcd2  16299  lcmgcdlem  16356  lcmftp  16386  exprmfct  16454  eulerthlem2  16528  dvdsprmpweqnn  16631  dvdsprmpweqle  16632  pcmpt  16638  vdwlem10  16736  cshwsidrepsw  16840  cshwshashlem1  16842  prmlem1a  16853  setsn0fun  16919  ressval3d  17001  ressval3dOLD  17002  mreexexd  17402  letsr  18356  insubm  18502  ghmghmrn  18898  pmtrfrn  19111  pmtr3ncom  19128  gsmtrcl  19169  psgnsn  19173  sylow1lem1  19248  efginvrel2  19378  efgsrel  19385  cntzcmnss  19487  gsum2dlem2  19617  telgsumfzs  19635  dprdval  19651  ablfac1eulem  19720  pgpfac1  19728  pgpfac  19732  srgpcomp  19813  ring1ne0  19875  rimf1o  20023  rimrhm  20024  brric2  20034  0ringnnzr  20585  zrhpsgnelbas  20844  psgndiflemA  20851  mplcoe1  21283  mplcoe3  21284  mplcoe5lem  21285  mplcoe5  21286  mpfaddcl  21360  mpfmulcl  21361  coe1ae0  21432  coe1fzgsumd  21518  gsummoncoe1  21520  pf1addcl  21564  pf1mulcl  21565  evl1gsumd  21568  mamufacex  21583  mat0dimcrng  21664  mavmulsolcl  21745  mdetunilem9  21814  cramerlem3  21883  pmatcollpw3fi1  21982  pm2mpfo  22008  chmaidscmat  22042  chfacfscmul0  22052  chfacfpmmul0  22056  cpmadugsumlemF  22070  tg2  22160  neindisj2  22319  neiptopnei  22328  t1t0  22544  fiuncmp  22600  hmeof1o  22960  ist1-5lem  23016  t1r0  23017  alexsublem  23240  imasdsf1olem  23571  tgioo  24004  fsumcn  24078  voliunlem3  24761  itgfsum  25036  dvbsss  25111  dvmptfsum  25184  dvfsumlem2  25236  dvfsumlem4  25238  plyco  25447  dgrcolem1  25479  dgrco  25481  dvntaylp  25575  taylthlem1  25577  jensen  26183  bposlem5  26481  lgsqrmodndvds  26546  gausslemma2dlem0i  26557  gausslemma2dlem4  26562  lgsquad2lem2  26578  2lgslem3  26597  2lgs  26600  2lgsoddprm  26609  dchrisum0flb  26703  pntpbnd1  26779  pntlemf  26798  brbtwn  27312  brcgr  27313  umgrnloopv  27521  umgrnloop  27523  usgrnloopvALT  27613  usgrnloopALT  27615  usgredg2vlem2  27638  subgrprop  27685  uvtxnbgrvtx  27805  cusgrsize2inds  27865  rgrprop  27972  rusgrprop  27974  wlkprop  28023  wlkvtxeledg  28036  wlkeq  28046  wlkl1loop  28050  wlk1walk  28051  uspgr2wlkeqi  28060  wlkreslem  28082  wlkres  28083  redwlk  28085  lfgrwlknloop  28102  2pthnloop  28144  usgr2trlncl  28173  usgr2pth  28177  clwlkcompim  28193  clwlkcompbp  28195  uspgrn2crct  28218  crctcshwlkn0  28231  wwlknp  28253  wwlkswwlksn  28275  wlkiswwlks2lem4  28282  wlkiswwlks2  28285  wlklnwwlkln2lem  28292  wwlksnext  28303  wwlksnextbi  28304  wwlksnredwwlkn0  28306  wwlksnextwrd  28307  clwlkclwwlklem2a  28407  clwlkclwwlklem2  28409  clwlkclwwlkflem  28413  clwwisshclwws  28424  clwwlknp  28446  clwwlknwwlksn  28447  clwwlkwwlksb  28463  clwwlkext2edg  28465  umgrhashecclwwlk  28487  clwwlknun  28521  1pthond  28553  upgr3v3e3cycl  28589  upgr4cycl4dv4e  28594  eupth2  28648  3vfriswmgr  28687  3cyclfrgrrn1  28694  n4cyclfrgr  28700  frgrnbnb  28702  frgrncvvdeqlem3  28710  frgrncvvdeqlem6  28713  frgrncvvdeqlem7  28714  frgrncvvdeqlem8  28715  frgrwopreglem4a  28719  frgrwopreg  28732  frgrregorufr0  28733  frgr2wwlkeqm  28740  2clwwlk2clwwlklem  28755  wlkl0  28776  frgrreggt1  28802  frgrregord013  28804  frgrregord13  28805  frgrogt3nreg  28806  friendshipgt3  28807  friendship  28808  blocn2  29215  cvexchlem  30775  cdj3lem2b  30844  cnvoprabOLD  31100  nnindf  31178  issgon  32136  sitgclg  32354  sseqp1  32407  bnj938  32962  bnj964  32968  bnj1052  33000  bnj1125  33017  subfacp1lem6  33192  cvmliftlem7  33298  cvmliftlem10  33301  mclsrcl  33568  madebdayim  34115  oldbdayim  34116  pprodss4v  34231  segleantisym  34462  rankeq1o  34518  bj-restv  35310  iooelexlt  35577  relowlssretop  35578  rdgeqoa  35585  matunitlindflem1  35817  poimirlem22  35843  poimirlem25  35846  poimirlem28  35849  poimirlem31  35852  mblfinlem3  35860  mbfresfi  35867  mettrifi  35959  opidon2OLD  36056  isexid2  36057  grpomndo  36077  elghomlem2OLD  36088  rngoidmlem  36138  rngoueqz  36142  iscringd  36200  cdlemk35s  38993  cdlemk39s  38995  cdlemk42  38997  uzindd  40027  mzpadd  40597  mzpmul  40598  mzpcompact2  40611  dford3lem2  40887  aomclem6  40922  cnsrexpcl  41028  ensucne0OLD  41175  pr2cv  41193  relexpss1d  41351  iunrelexpmin1  41354  iunrelexpmin2  41358  tfindsd  41861  nzin  41974  axc11next  42062  iotavalsb  42089  ssdec  42676  fperiodmullem  42890  monoordxrv  43070  fmul01  43170  fmulcl  43171  fmuldfeqlem1  43172  fmuldfeq  43173  fprodcnlem  43189  iblspltprt  43563  itgspltprt  43569  stoweidlem2  43592  stoweidlem3  43593  stoweidlem6  43596  stoweidlem8  43598  stoweidlem17  43607  stoweidlem19  43609  stoweidlem21  43611  stoweidlem26  43616  stoweidlem31  43621  stoweidlem43  43633  fourierdlem42  43739  funressnfv  44595  eu2ndop1stv  44675  afv0fv0  44699  afv0nbfvbi  44701  funressnbrafv2  44794  funbrafv2  44797  nelbrim  44825  ssfz12  44864  fzoopth  44877  smonoord  44881  iccpartiltu  44932  iccpartigtl  44933  iccelpart  44943  icceuelpart  44946  fargshiftf  44950  fargshiftf1  44951  fargshiftfo  44952  sprel  44994  sprsymrelf1lem  45001  sprsymrelfolem2  45003  prproropf1olem4  45016  lighneallem4  45120  mogoldbblem  45230  fpprnn  45240  fpprwppr  45249  fpprwpprb  45250  sbgoldbwt  45287  bgoldbtbndlem2  45316  bgoldbtbndlem4  45318  tgoldbach  45327  upwlkwlk  45359  clcllaw  45443  intop  45455  clintop  45460  assintop  45461  assintopcllaw  45464  lmod0rng  45484  ringrng  45495  rngimf1o  45521  rngimrnghm  45522  ztprmneprm  45741  scmsuppss  45766  ply1mulgsumlem1  45785  ply1mulgsumlem2  45786  lcoel0  45827  ellcoellss  45834  lindslinindsimp2lem5  45861  ldepspr  45872  flnn0div2ge  45937  nnolog2flm1  45994  blengt1fldiv2p1  45997  dignn0flhalf  46022  naryfvalelfv  46036  0aryfvalelfv  46039  fv1arycl  46041  fv2arycl  46052