MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpcom Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mpcom.1 . 2 (𝜓𝜑)
2 mpcom.2 . . 3 (𝜑 → (𝜓𝜒))
32com12 32 . 2 (𝜓 → (𝜑𝜒))
41, 3mpd 15 1 (𝜓𝜒)
Colors of variables: wff setvar class
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  2429  mo4  2554  sbcn1  3829  sbcim1  3830  sbcim1OLD  3831  sbcbi1  3835  sbcel21v  3846  csbie2df  4442  elimasni  6096  sotri  6134  unixpid  6290  f0rn0  6782  f1ocnv  6850  funbrfv  6947  elfvmptrab1w  7031  f1dom3el3dif  7279  oprabidw  7450  oprabid  7451  oprabv  7480  ndmovordi  7612  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  elovmpt3rab1  7681  limomss  7876  unielxp  8032  bropfvvvvlem  8096  f1o2ndf1  8127  smogt  8388  tfrlem1  8397  oawordeulem  8575  omass  8601  ecopovtrn  8839  mapfvd  8898  findcard2d  9191  ssfi  9198  f1domfi  9209  php  9235  phpOLD  9247  unxpdom  9278  findcard3  9310  findcard3OLD  9311  isfinite2  9326  fsuppimp  9394  fsuppunfi  9413  fsuppunbi  9414  fsuppres  9418  infsupprpr  9529  cantnfval2  9694  cantnfle  9696  cantnfp1lem3  9705  cantnflem1  9714  cnfcom  9725  rankr1ai  9823  rankonidlem  9853  rankxplim2  9905  oncard  9985  ficardom  9986  cardne  9990  acnnum  10077  alephord2i  10102  cardaleph  10114  aceq3lem  10145  dfac5lem5  10152  dfac12lem3  10170  ackbij1lem16  10260  cfslb  10291  cfslb2n  10293  cfsmolem  10295  fin4i  10323  infpssr  10333  fin1a2lem6  10430  axdc3lem2  10476  axcclem  10482  ttukeylem6  10539  fodomb  10551  gchi  10649  fpwwe2lem4  10659  pwfseqlem4  10687  pwfseq  10689  inawina  10715  wunfi  10746  inar1  10800  ltexnq  11000  ltbtwnnq  11003  ltexprlem4  11064  ltexpri  11068  prlem936  11072  suplem1pr  11077  suplem2pr  11078  recexsrlem  11128  mulgt0sr  11130  map2psrpr  11135  supsr  11137  eqlei  11356  eqlei2  11357  ledivp1i  12172  nnind  12263  nnmulcl  12269  nn0ge2m1nn  12574  nnnegz  12594  ublbneg  12950  xmulasslem  13299  ixxssixx  13373  iccshftri  13499  iccshftli  13501  iccdili  13503  icccntri  13505  elfz1b  13605  fzo1fzo0n0  13718  elfzonlteqm1  13743  elfzo0l  13757  ssfzo12  13760  fzoopth  13763  elfzo1elm1fzo0  13769  elfzr  13781  elfzlmr  13782  zmodidfzoimp  13902  mptnn0fsuppr  14000  seqp1  14017  seqcl2  14021  seqfveq2  14025  seqshft2  14029  monoord  14033  seqsplit  14036  seqcaopr3  14038  seqf1olem2a  14041  seqf1o  14044  seqid2  14049  seqhomo  14050  hashf1rn  14347  hashinfxadd  14380  hashf1lem2  14453  seqcoll  14461  hash2pr  14466  pr2pwpr  14476  hashge2el2difr  14478  hash3tr  14487  fi1uzind  14494  brfi1indALT  14497  elovmptnn0wrd  14545  swrdswrd  14691  pfxccatin12lem2a  14713  swrdccat  14721  swrdccatin1d  14729  swrdccatin2d  14730  repswccat  14772  cshwidxmod  14789  relexpsucnnr  15008  rtrclreclem3  15043  rtrclreclem4  15044  dfrtrcl2  15045  relexpindlem  15046  relexpind  15047  rtrclind  15048  cjre  15122  climeu  15535  climub  15644  fsum2d  15753  fsumabs  15783  fsumrlim  15793  fsumo1  15794  fsumiun  15803  prodfn0  15876  prodfrec  15877  ntrivcvg  15879  fprodabs  15954  fprod2d  15961  fprodefsum  16075  ruclem9  16218  dvdsmod0  16240  p1modz1  16241  dvdsmodexp  16242  dvdsabseq  16293  mod2eq1n2dvds  16327  mulsucdiv2z  16333  nno  16362  nn0o  16363  sadcadd  16436  sadadd2  16438  saddisjlem  16442  smuval2  16460  smupval  16466  smueqlem  16468  smumullem  16470  dfgcd2  16525  lcmgcdlem  16580  lcmftp  16610  exprmfct  16678  eulerthlem2  16754  dvdsprmpweqnn  16857  dvdsprmpweqle  16858  pcmpt  16864  vdwlem10  16962  cshwsidrepsw  17066  cshwshashlem1  17068  prmlem1a  17079  setsn0fun  17145  ressval3d  17230  ressval3dOLD  17231  mreexexd  17631  letsr  18588  insubm  18778  ghmghmrn  19198  pmtrfrn  19425  pmtr3ncom  19442  gsmtrcl  19483  psgnsn  19487  sylow1lem1  19565  efginvrel2  19694  efgsrel  19701  cntzcmnss  19808  gsum2dlem2  19938  telgsumfzs  19956  dprdval  19972  ablfac1eulem  20041  pgpfac1  20049  pgpfac  20053  srgpcomp  20170  ringrng  20233  ring1ne0  20247  rngimf1o  20405  rngimrnghm  20406  rngimcnv  20407  0ringnnzr  20474  zrhpsgnelbas  21543  psgndiflemA  21550  mplcoe1  21997  mplcoe3  21998  mplcoe5lem  21999  mplcoe5  22000  mpfaddcl  22073  mpfmulcl  22074  coe1ae0  22159  coe1fzgsumd  22248  gsummoncoe1  22252  pf1addcl  22297  pf1mulcl  22298  evl1gsumd  22301  mamufacex  22340  mat0dimcrng  22416  mavmulsolcl  22497  mdetunilem9  22566  cramerlem3  22635  pmatcollpw3fi1  22734  pm2mpfo  22760  chmaidscmat  22794  chfacfscmul0  22804  chfacfpmmul0  22808  cpmadugsumlemF  22822  tg2  22912  neindisj2  23071  neiptopnei  23080  t1t0  23296  fiuncmp  23352  hmeof1o  23712  ist1-5lem  23768  t1r0  23769  alexsublem  23992  imasdsf1olem  24323  tgioo  24756  fsumcn  24832  voliunlem3  25525  itgfsum  25800  dvbsss  25875  dvmptfsum  25951  dvfsumlem2  26005  dvfsumlem2OLD  26006  dvfsumlem4  26008  plyco  26220  dgrcolem1  26253  dgrco  26255  dvntaylp  26351  taylthlem1  26353  jensen  26966  bposlem5  27266  lgsqrmodndvds  27331  gausslemma2dlem0i  27342  gausslemma2dlem4  27347  lgsquad2lem2  27363  2lgslem3  27382  2lgs  27385  2lgsoddprm  27394  dchrisum0flb  27488  pntpbnd1  27564  pntlemf  27583  madebdayim  27860  oldbdayim  27861  brbtwn  28782  brcgr  28783  umgrnloopv  28991  umgrnloop  28993  usgrnloopvALT  29086  usgrnloopALT  29088  usgredg2vlem2  29111  subgrprop  29158  uvtxnbgrvtx  29278  cusgrsize2inds  29339  rgrprop  29446  rusgrprop  29448  wlkprop  29497  wlkvtxeledg  29510  wlkeq  29520  wlkl1loop  29524  wlk1walk  29525  uspgr2wlkeqi  29534  wlkreslem  29555  wlkres  29556  redwlk  29558  lfgrwlknloop  29575  2pthnloop  29617  usgr2trlncl  29646  usgr2pth  29650  clwlkcompim  29666  clwlkcompbp  29668  uspgrn2crct  29691  crctcshwlkn0  29704  wwlknp  29726  wwlkswwlksn  29748  wlkiswwlks2lem4  29755  wlkiswwlks2  29758  wlklnwwlkln2lem  29765  wwlksnext  29776  wwlksnextbi  29777  wwlksnredwwlkn0  29779  wwlksnextwrd  29780  clwlkclwwlklem2a  29880  clwlkclwwlklem2  29882  clwlkclwwlkflem  29886  clwwisshclwws  29897  clwwlknp  29919  clwwlknwwlksn  29920  clwwlkwwlksb  29936  clwwlkext2edg  29938  umgrhashecclwwlk  29960  clwwlknun  29994  1pthond  30026  upgr3v3e3cycl  30062  upgr4cycl4dv4e  30067  eupth2  30121  3vfriswmgr  30160  3cyclfrgrrn1  30167  n4cyclfrgr  30173  frgrnbnb  30175  frgrncvvdeqlem3  30183  frgrncvvdeqlem6  30186  frgrncvvdeqlem7  30187  frgrncvvdeqlem8  30188  frgrwopreglem4a  30192  frgrwopreg  30205  frgrregorufr0  30206  frgr2wwlkeqm  30213  2clwwlk2clwwlklem  30228  wlkl0  30249  frgrreggt1  30275  frgrregord013  30277  frgrregord13  30278  frgrogt3nreg  30279  friendshipgt3  30280  friendship  30281  blocn2  30690  cvexchlem  32250  cdj3lem2b  32319  cnvoprabOLD  32584  nnindf  32667  domnprodn0  33065  issgon  33873  sitgclg  34093  sseqp1  34146  bnj938  34699  bnj964  34705  bnj1052  34737  bnj1125  34754  subfacp1lem6  34926  cvmliftlem7  35032  cvmliftlem10  35035  mclsrcl  35302  pprodss4v  35611  segleantisym  35842  rankeq1o  35898  bj-restv  36705  iooelexlt  36972  relowlssretop  36973  rdgeqoa  36980  matunitlindflem1  37220  poimirlem22  37246  poimirlem25  37249  poimirlem28  37252  poimirlem31  37255  mblfinlem3  37263  mbfresfi  37270  mettrifi  37361  opidon2OLD  37458  isexid2  37459  grpomndo  37479  elghomlem2OLD  37490  rngoidmlem  37540  rngoueqz  37544  iscringd  37602  cdlemk35s  40540  cdlemk39s  40542  cdlemk42  40544  uzindd  41579  mzpadd  42300  mzpmul  42301  mzpcompact2  42314  dford3lem2  42590  aomclem6  42625  cnsrexpcl  42731  ensucne0OLD  43102  pr2cv  43120  relexpss1d  43277  iunrelexpmin1  43280  iunrelexpmin2  43284  tfindsd  43784  nzin  43897  axc11next  43985  iotavalsb  44012  ssdec  44594  fperiodmullem  44823  monoordxrv  45002  fmul01  45106  fmulcl  45107  fmuldfeqlem1  45108  fmuldfeq  45109  iblspltprt  45499  itgspltprt  45505  stoweidlem2  45528  stoweidlem3  45529  stoweidlem6  45532  stoweidlem8  45534  stoweidlem17  45543  stoweidlem19  45545  stoweidlem21  45547  stoweidlem26  45552  stoweidlem31  45557  stoweidlem43  45569  fourierdlem42  45675  funressnfv  46563  eu2ndop1stv  46643  afv0fv0  46667  afv0nbfvbi  46669  funressnbrafv2  46762  funbrafv2  46765  nelbrim  46793  ssfz12  46832  smonoord  46848  iccpartiltu  46899  iccpartigtl  46900  iccelpart  46910  icceuelpart  46913  fargshiftf  46917  fargshiftf1  46918  fargshiftfo  46919  sprel  46961  sprsymrelf1lem  46968  sprsymrelfolem2  46970  prproropf1olem4  46983  lighneallem4  47087  mogoldbblem  47197  fpprnn  47207  fpprwppr  47216  fpprwpprb  47217  sbgoldbwt  47254  bgoldbtbndlem2  47283  bgoldbtbndlem4  47285  tgoldbach  47294  grimprop  47353  upwlkwlk  47387  clcllaw  47439  intop  47451  clintop  47456  assintop  47457  assintopcllaw  47460  lmod0rng  47477  ztprmneprm  47597  scmsuppss  47622  ply1mulgsumlem1  47640  ply1mulgsumlem2  47641  lcoel0  47682  ellcoellss  47689  lindslinindsimp2lem5  47716  ldepspr  47727  flnn0div2ge  47792  nnolog2flm1  47849  blengt1fldiv2p1  47852  dignn0flhalf  47877  naryfvalelfv  47891  0aryfvalelfv  47894  fv1arycl  47896  fv2arycl  47907
  Copyright terms: Public domain W3C validator