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  2441  mo4  2567  sbcn1  3795  sbcim1  3796  sbcbi1  3800  sbcel21v  3810  sbccomlem  3821  csbie2df  4397  elimasni  6058  sotri  6092  unixpid  6250  f0rn0  6727  f1ocnv  6794  funbrfv  6890  elfvmptrab1w  6977  f1dom3el3dif  7225  oprabidw  7399  oprabid  7400  oprabv  7428  ndmovordi  7559  elovmporab  7614  elovmporab1w  7615  elovmporab1  7616  elovmpt3rab1  7628  limomss  7823  unielxp  7981  bropfvvvvlem  8043  f1o2ndf1  8074  smogt  8309  tfrlem1  8317  oawordeulem  8491  omass  8517  ecopovtrn  8769  mapfvd  8829  findcard2d  9103  ssfi  9109  f1domfi  9117  php  9143  unxpdom  9171  findcard3  9195  isfinite2  9210  fsuppimp  9283  fsuppunfi  9303  fsuppunbi  9304  fsuppres  9308  infsupprpr  9421  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  11255  eqlei2  11256  ledivp1i  12079  nnind  12175  nnmulcl  12181  nn0ge2m1nn  12483  nnnegz  12503  ublbneg  12858  xmulasslem  13212  ixxssixx  13287  iccshftri  13415  iccshftli  13417  iccdili  13419  icccntri  13421  elfz1b  13521  fzo1fzo0n0  13643  elfzonlteqm1  13669  elfzo0l  13684  ssfzo12  13687  fzoopth  13690  elfzo1elm1fzo0  13696  elfzr  13709  elfzlmr  13710  zmodidfzoimp  13833  mptnn0fsuppr  13934  seqp1  13951  seqcl2  13955  seqfveq2  13959  seqshft2  13963  monoord  13967  seqsplit  13970  seqcaopr3  13972  seqf1olem2a  13975  seqf1o  13978  seqid2  13983  seqhomo  13984  hashf1rn  14287  hashinfxadd  14320  hashf1lem2  14391  seqcoll  14399  hash2pr  14404  pr2pwpr  14414  hashge2el2difr  14416  hash3tr  14426  fi1uzind  14442  brfi1indALT  14445  elovmptnn0wrd  14494  swrdswrd  14640  pfxccatin12lem2a  14662  swrdccat  14670  swrdccatin1d  14678  swrdccatin2d  14679  repswccat  14721  cshwidxmod  14738  relexpsucnnr  14960  rtrclreclem3  14995  rtrclreclem4  14996  dfrtrcl2  14997  relexpindlem  14998  relexpind  14999  rtrclind  15000  cjre  15074  climeu  15490  climub  15597  fsum2d  15706  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  prodfn0  15829  prodfrec  15830  ntrivcvg  15832  fprodabs  15909  fprod2d  15916  fprodefsum  16030  ruclem9  16175  dvdsmod0  16197  p1modz1  16198  dvdsmodexp  16199  dvdsabseq  16252  mod2eq1n2dvds  16286  mulsucdiv2z  16292  nno  16321  nn0o  16322  sadcadd  16397  sadadd2  16399  saddisjlem  16403  smuval2  16421  smupval  16427  smueqlem  16429  smumullem  16431  dfgcd2  16485  lcmgcdlem  16545  lcmftp  16575  exprmfct  16643  eulerthlem2  16721  dvdsprmpweqnn  16825  dvdsprmpweqle  16826  pcmpt  16832  vdwlem10  16930  cshwsidrepsw  17033  cshwshashlem1  17035  prmlem1a  17046  setsn0fun  17112  ressval3d  17185  mreexexd  17583  letsr  18528  insubm  18755  ghmghmrn  19176  pmtrfrn  19399  pmtr3ncom  19416  gsmtrcl  19457  psgnsn  19461  sylow1lem1  19539  efginvrel2  19668  efgsrel  19675  cntzcmnss  19782  gsum2dlem2  19912  telgsumfzs  19930  dprdval  19946  ablfac1eulem  20015  pgpfac1  20023  pgpfac  20027  srgpcomp  20165  ringrng  20232  ring1ne0  20246  rngimf1o  20402  rngimrnghm  20403  rngimcnv  20404  0ringnnzr  20470  zrhpsgnelbas  21561  psgndiflemA  21568  mplcoe1  22004  mplcoe3  22005  mplcoe5lem  22006  mplcoe5  22007  mpfaddcl  22080  mpfmulcl  22081  coe1ae0  22169  coe1fzgsumd  22260  gsummoncoe1  22264  pf1addcl  22309  pf1mulcl  22310  evl1gsumd  22313  mamufacex  22352  mat0dimcrng  22426  mavmulsolcl  22507  mdetunilem9  22576  cramerlem3  22645  pmatcollpw3fi1  22744  pm2mpfo  22770  chmaidscmat  22804  chfacfscmul0  22814  chfacfpmmul0  22818  cpmadugsumlemF  22832  tg2  22921  neindisj2  23079  neiptopnei  23088  t1t0  23304  fiuncmp  23360  hmeof1o  23720  ist1-5lem  23776  t1r0  23777  alexsublem  24000  imasdsf1olem  24329  tgioo  24752  fsumcn  24829  voliunlem3  25521  itgfsum  25796  dvbsss  25871  dvmptfsum  25947  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem4  26004  plyco  26214  dgrcolem1  26247  dgrco  26249  dvntaylp  26347  taylthlem1  26349  jensen  26967  bposlem5  27267  lgsqrmodndvds  27332  gausslemma2dlem0i  27343  gausslemma2dlem4  27348  lgsquad2lem2  27364  2lgslem3  27383  2lgs  27386  2lgsoddprm  27395  dchrisum0flb  27489  pntpbnd1  27565  pntlemf  27584  madebdayim  27896  oldbdayim  27897  pw2cut  28468  brbtwn  28984  brcgr  28985  umgrnloopv  29191  umgrnloop  29193  usgrnloopvALT  29286  usgrnloopALT  29288  usgredg2vlem2  29311  subgrprop  29358  uvtxnbgrvtx  29478  cusgrsize2inds  29539  rgrprop  29646  rusgrprop  29648  wlkprop  29697  wlkvtxeledg  29709  wlkeq  29719  wlkl1loop  29723  wlk1walk  29724  uspgr2wlkeqi  29733  wlkreslem  29753  wlkres  29754  redwlk  29756  lfgrwlknloop  29773  2pthnloop  29816  usgr2trlncl  29845  usgr2pth  29849  clwlkcompim  29865  clwlkcompbp  29867  uspgrn2crct  29893  crctcshwlkn0  29906  wwlknp  29928  wwlkswwlksn  29950  wlkiswwlks2lem4  29957  wlkiswwlks2  29960  wlklnwwlkln2lem  29967  wwlksnext  29978  wwlksnextbi  29979  wwlksnredwwlkn0  29981  wwlksnextwrd  29982  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlkflem  30091  clwwisshclwws  30102  clwwlknp  30124  clwwlknwwlksn  30125  clwwlkwwlksb  30141  clwwlkext2edg  30143  umgrhashecclwwlk  30165  clwwlknun  30199  1pthond  30231  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  eupth2  30326  3vfriswmgr  30365  3cyclfrgrrn1  30372  n4cyclfrgr  30378  frgrnbnb  30380  frgrncvvdeqlem3  30388  frgrncvvdeqlem6  30391  frgrncvvdeqlem7  30392  frgrncvvdeqlem8  30393  frgrwopreglem4a  30397  frgrwopreg  30410  frgrregorufr0  30411  frgr2wwlkeqm  30418  2clwwlk2clwwlklem  30433  wlkl0  30454  frgrreggt1  30480  frgrregord013  30482  frgrregord13  30483  frgrogt3nreg  30484  friendshipgt3  30485  friendship  30486  blocn2  30895  cvexchlem  32455  cdj3lem2b  32524  nnindf  32910  gsumwun  33169  domnprodn0  33368  issgon  34300  sitgclg  34519  sseqp1  34572  bnj938  35112  bnj964  35118  bnj1052  35150  bnj1125  35167  onvf1odlem4  35319  subfacp1lem6  35398  cvmliftlem7  35504  cvmliftlem10  35507  mclsrcl  35774  pprodss4v  36095  segleantisym  36328  rankeq1o  36384  bj-restv  37342  iooelexlt  37611  relowlssretop  37612  rdgeqoa  37619  matunitlindflem1  37861  poimirlem22  37887  poimirlem25  37890  poimirlem28  37893  poimirlem31  37896  mblfinlem3  37904  mbfresfi  37911  mettrifi  38002  opidon2OLD  38099  isexid2  38100  grpomndo  38120  elghomlem2OLD  38131  rngoidmlem  38181  rngoueqz  38185  iscringd  38243  cdlemk35s  41307  cdlemk39s  41309  cdlemk42  41311  uzindd  42341  mzpadd  43089  mzpmul  43090  mzpcompact2  43103  dford3lem2  43378  aomclem6  43410  cnsrexpcl  43516  ensucne0OLD  43880  pr2cv  43898  relexpss1d  44055  iunrelexpmin1  44058  iunrelexpmin2  44062  tfindsd  44560  nzin  44668  axc11next  44756  iotavalsb  44783  ssdec  45441  fperiodmullem  45659  monoordxrv  45833  fmul01  45934  fmulcl  45935  fmuldfeqlem1  45936  fmuldfeq  45937  iblspltprt  46325  itgspltprt  46331  stoweidlem2  46354  stoweidlem3  46355  stoweidlem6  46358  stoweidlem8  46360  stoweidlem17  46369  stoweidlem19  46371  stoweidlem21  46373  stoweidlem26  46378  stoweidlem31  46383  stoweidlem43  46395  fourierdlem42  46501  funressnfv  47397  eu2ndop1stv  47479  afv0fv0  47503  afv0nbfvbi  47505  funressnbrafv2  47598  funbrafv2  47601  nelbrim  47629  ssfz12  47668  smonoord  47725  iccpartiltu  47776  iccpartigtl  47777  iccelpart  47787  icceuelpart  47790  fargshiftf  47794  fargshiftf1  47795  fargshiftfo  47796  sprel  47838  sprsymrelf1lem  47845  sprsymrelfolem2  47847  prproropf1olem4  47860  lighneallem4  47964  mogoldbblem  48074  fpprnn  48084  fpprwppr  48093  fpprwpprb  48094  sbgoldbwt  48131  bgoldbtbndlem2  48160  bgoldbtbndlem4  48162  tgoldbach  48171  grimprop  48237  grlimprop  48338  grilcbri2  48365  upwlkwlk  48493  clcllaw  48545  intop  48557  clintop  48562  assintop  48563  assintopcllaw  48566  lmod0rng  48583  ztprmneprm  48701  scmsuppss  48725  ply1mulgsumlem1  48740  ply1mulgsumlem2  48741  lcoel0  48782  ellcoellss  48789  lindslinindsimp2lem5  48816  ldepspr  48827  flnn0div2ge  48887  nnolog2flm1  48944  blengt1fldiv2p1  48947  dignn0flhalf  48972  naryfvalelfv  48986  0aryfvalelfv  48989  fv1arycl  48991  fv2arycl  49002