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  3782  sbcim1  3783  sbcbi1  3787  sbcel21v  3797  sbccomlem  3808  csbie2df  4384  elimasni  6048  sotri  6082  unixpid  6240  f0rn0  6717  f1ocnv  6784  funbrfv  6880  elfvmptrab1w  6967  f1dom3el3dif  7215  oprabidw  7389  oprabid  7390  oprabv  7418  ndmovordi  7549  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  elovmpt3rab1  7618  limomss  7813  unielxp  7971  bropfvvvvlem  8032  f1o2ndf1  8063  smogt  8298  tfrlem1  8306  oawordeulem  8480  omass  8506  ecopovtrn  8758  mapfvd  8818  findcard2d  9092  ssfi  9098  f1domfi  9106  php  9132  unxpdom  9160  findcard3  9184  isfinite2  9199  fsuppimp  9272  fsuppunfi  9292  fsuppunbi  9293  fsuppres  9297  infsupprpr  9410  cantnfval2  9579  cantnfle  9581  cantnfp1lem3  9590  cantnflem1  9599  cnfcom  9610  rankr1ai  9711  rankonidlem  9741  rankxplim2  9793  oncard  9873  ficardom  9874  cardne  9878  acnnum  9963  alephord2i  9988  cardaleph  10000  aceq3lem  10031  dfac5lem5  10038  dfac12lem3  10057  ackbij1lem16  10145  cfslb  10177  cfslb2n  10179  cfsmolem  10181  fin4i  10209  infpssr  10219  fin1a2lem6  10316  axdc3lem2  10362  axcclem  10368  ttukeylem6  10425  fodomb  10437  gchi  10536  pwfseq  10576  inawina  10602  wunfi  10633  inar1  10687  ltexnq  10887  ltbtwnnq  10890  ltexprlem4  10951  ltexpri  10955  prlem936  10959  suplem1pr  10964  suplem2pr  10965  recexsrlem  11015  mulgt0sr  11017  map2psrpr  11022  supsr  11024  eqlei  11244  eqlei2  11245  ledivp1i  12068  nnind  12164  nnmulcl  12170  nn0ge2m1nn  12472  nnnegz  12492  ublbneg  12847  xmulasslem  13201  ixxssixx  13276  iccshftri  13404  iccshftli  13406  iccdili  13408  icccntri  13410  elfz1b  13510  fzo1fzo0n0  13632  elfzonlteqm1  13658  elfzo0l  13673  ssfzo12  13676  fzoopth  13679  elfzo1elm1fzo0  13685  elfzr  13698  elfzlmr  13699  zmodidfzoimp  13822  mptnn0fsuppr  13923  seqp1  13940  seqcl2  13944  seqfveq2  13948  seqshft2  13952  monoord  13956  seqsplit  13959  seqcaopr3  13961  seqf1olem2a  13964  seqf1o  13967  seqid2  13972  seqhomo  13973  hashf1rn  14276  hashinfxadd  14309  hashf1lem2  14380  seqcoll  14388  hash2pr  14393  pr2pwpr  14403  hashge2el2difr  14405  hash3tr  14415  fi1uzind  14431  brfi1indALT  14434  elovmptnn0wrd  14483  swrdswrd  14629  pfxccatin12lem2a  14651  swrdccat  14659  swrdccatin1d  14667  swrdccatin2d  14668  repswccat  14710  cshwidxmod  14727  relexpsucnnr  14949  rtrclreclem3  14984  rtrclreclem4  14985  dfrtrcl2  14986  relexpindlem  14987  relexpind  14988  rtrclind  14989  cjre  15063  climeu  15479  climub  15586  fsum2d  15695  fsumabs  15725  fsumrlim  15735  fsumo1  15736  fsumiun  15745  prodfn0  15818  prodfrec  15819  ntrivcvg  15821  fprodabs  15898  fprod2d  15905  fprodefsum  16019  ruclem9  16164  dvdsmod0  16186  p1modz1  16187  dvdsmodexp  16188  dvdsabseq  16241  mod2eq1n2dvds  16275  mulsucdiv2z  16281  nno  16310  nn0o  16311  sadcadd  16386  sadadd2  16388  saddisjlem  16392  smuval2  16410  smupval  16416  smueqlem  16418  smumullem  16420  dfgcd2  16474  lcmgcdlem  16534  lcmftp  16564  exprmfct  16632  eulerthlem2  16710  dvdsprmpweqnn  16814  dvdsprmpweqle  16815  pcmpt  16821  vdwlem10  16919  cshwsidrepsw  17022  cshwshashlem1  17024  prmlem1a  17035  setsn0fun  17101  ressval3d  17174  mreexexd  17572  letsr  18517  insubm  18744  ghmghmrn  19168  pmtrfrn  19391  pmtr3ncom  19408  gsmtrcl  19449  psgnsn  19453  sylow1lem1  19531  efginvrel2  19660  efgsrel  19667  cntzcmnss  19774  gsum2dlem2  19904  telgsumfzs  19922  dprdval  19938  ablfac1eulem  20007  pgpfac1  20015  pgpfac  20019  srgpcomp  20157  ringrng  20224  ring1ne0  20238  rngimf1o  20392  rngimrnghm  20393  rngimcnv  20394  0ringnnzr  20460  zrhpsgnelbas  21551  psgndiflemA  21558  mplcoe1  21993  mplcoe3  21994  mplcoe5lem  21995  mplcoe5  21996  mpfaddcl  22069  mpfmulcl  22070  coe1ae0  22158  coe1fzgsumd  22247  gsummoncoe1  22251  pf1addcl  22296  pf1mulcl  22297  evl1gsumd  22300  mamufacex  22339  mat0dimcrng  22413  mavmulsolcl  22494  mdetunilem9  22563  cramerlem3  22632  pmatcollpw3fi1  22731  pm2mpfo  22757  chmaidscmat  22791  chfacfscmul0  22801  chfacfpmmul0  22805  cpmadugsumlemF  22819  tg2  22908  neindisj2  23066  neiptopnei  23075  t1t0  23291  fiuncmp  23347  hmeof1o  23707  ist1-5lem  23763  t1r0  23764  alexsublem  23987  imasdsf1olem  24316  tgioo  24739  fsumcn  24815  voliunlem3  25497  itgfsum  25772  dvbsss  25847  dvmptfsum  25920  dvfsumlem2  25974  dvfsumlem2OLD  25975  dvfsumlem4  25977  plyco  26187  dgrcolem1  26219  dgrco  26221  dvntaylp  26319  taylthlem1  26321  jensen  26939  bposlem5  27239  lgsqrmodndvds  27304  gausslemma2dlem0i  27315  gausslemma2dlem4  27320  lgsquad2lem2  27336  2lgslem3  27355  2lgs  27358  2lgsoddprm  27367  dchrisum0flb  27461  pntpbnd1  27537  pntlemf  27556  madebdayim  27868  oldbdayim  27869  pw2cut  28440  brbtwn  28956  brcgr  28957  umgrnloopv  29163  umgrnloop  29165  usgrnloopvALT  29258  usgrnloopALT  29260  usgredg2vlem2  29283  subgrprop  29330  uvtxnbgrvtx  29450  cusgrsize2inds  29511  rgrprop  29618  rusgrprop  29620  wlkprop  29669  wlkvtxeledg  29681  wlkeq  29691  wlkl1loop  29695  wlk1walk  29696  uspgr2wlkeqi  29705  wlkreslem  29725  wlkres  29726  redwlk  29728  lfgrwlknloop  29745  2pthnloop  29788  usgr2trlncl  29817  usgr2pth  29821  clwlkcompim  29837  clwlkcompbp  29839  uspgrn2crct  29865  crctcshwlkn0  29878  wwlknp  29900  wwlkswwlksn  29922  wlkiswwlks2lem4  29929  wlkiswwlks2  29932  wlklnwwlkln2lem  29939  wwlksnext  29950  wwlksnextbi  29951  wwlksnredwwlkn0  29953  wwlksnextwrd  29954  clwlkclwwlklem2a  30057  clwlkclwwlklem2  30059  clwlkclwwlkflem  30063  clwwisshclwws  30074  clwwlknp  30096  clwwlknwwlksn  30097  clwwlkwwlksb  30113  clwwlkext2edg  30115  umgrhashecclwwlk  30137  clwwlknun  30171  1pthond  30203  upgr3v3e3cycl  30239  upgr4cycl4dv4e  30244  eupth2  30298  3vfriswmgr  30337  3cyclfrgrrn1  30344  n4cyclfrgr  30350  frgrnbnb  30352  frgrncvvdeqlem3  30360  frgrncvvdeqlem6  30363  frgrncvvdeqlem7  30364  frgrncvvdeqlem8  30365  frgrwopreglem4a  30369  frgrwopreg  30382  frgrregorufr0  30383  frgr2wwlkeqm  30390  2clwwlk2clwwlklem  30405  wlkl0  30426  frgrreggt1  30452  frgrregord013  30454  frgrregord13  30455  frgrogt3nreg  30456  friendshipgt3  30457  friendship  30458  blocn2  30868  cvexchlem  32428  cdj3lem2b  32497  nnindf  32883  gsumwun  33142  domnprodn0  33341  issgon  34273  sitgclg  34492  sseqp1  34545  bnj938  35085  bnj964  35091  bnj1052  35123  bnj1125  35140  onvf1odlem4  35294  subfacp1lem6  35373  cvmliftlem7  35479  cvmliftlem10  35482  mclsrcl  35749  pprodss4v  36070  segleantisym  36303  rankeq1o  36359  bj-restv  37405  iooelexlt  37674  relowlssretop  37675  rdgeqoa  37682  matunitlindflem1  37928  poimirlem22  37954  poimirlem25  37957  poimirlem28  37960  poimirlem31  37963  mblfinlem3  37971  mbfresfi  37978  mettrifi  38069  opidon2OLD  38166  isexid2  38167  grpomndo  38187  elghomlem2OLD  38198  rngoidmlem  38248  rngoueqz  38252  iscringd  38310  cdlemk35s  41374  cdlemk39s  41376  cdlemk42  41378  uzindd  42408  mzpadd  43169  mzpmul  43170  mzpcompact2  43183  dford3lem2  43458  aomclem6  43490  cnsrexpcl  43596  ensucne0OLD  43960  pr2cv  43978  relexpss1d  44135  iunrelexpmin1  44138  iunrelexpmin2  44142  tfindsd  44640  nzin  44748  axc11next  44836  iotavalsb  44863  ssdec  45521  fperiodmullem  45739  monoordxrv  45913  fmul01  46014  fmulcl  46015  fmuldfeqlem1  46016  fmuldfeq  46017  iblspltprt  46405  itgspltprt  46411  stoweidlem2  46434  stoweidlem3  46435  stoweidlem6  46438  stoweidlem8  46440  stoweidlem17  46449  stoweidlem19  46451  stoweidlem21  46453  stoweidlem26  46458  stoweidlem31  46463  stoweidlem43  46475  fourierdlem42  46581  funressnfv  47477  eu2ndop1stv  47559  afv0fv0  47583  afv0nbfvbi  47585  funressnbrafv2  47678  funbrafv2  47681  nelbrim  47709  ssfz12  47748  smonoord  47805  iccpartiltu  47856  iccpartigtl  47857  iccelpart  47867  icceuelpart  47870  fargshiftf  47874  fargshiftf1  47875  fargshiftfo  47876  sprel  47918  sprsymrelf1lem  47925  sprsymrelfolem2  47927  prproropf1olem4  47940  lighneallem4  48044  mogoldbblem  48154  fpprnn  48164  fpprwppr  48173  fpprwpprb  48174  sbgoldbwt  48211  bgoldbtbndlem2  48240  bgoldbtbndlem4  48242  tgoldbach  48251  grimprop  48317  grlimprop  48418  grilcbri2  48445  upwlkwlk  48573  clcllaw  48625  intop  48637  clintop  48642  assintop  48643  assintopcllaw  48646  lmod0rng  48663  ztprmneprm  48781  scmsuppss  48805  ply1mulgsumlem1  48820  ply1mulgsumlem2  48821  lcoel0  48862  ellcoellss  48869  lindslinindsimp2lem5  48896  ldepspr  48907  flnn0div2ge  48967  nnolog2flm1  49024  blengt1fldiv2p1  49027  dignn0flhalf  49052  naryfvalelfv  49066  0aryfvalelfv  49069  fv1arycl  49071  fv2arycl  49082