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:  syldan  487  axc16i  2321  sbcn1  3479  sbcim1  3480  sbcbi1  3481  sbcel21v  3495  elimasni  5490  sotri  5521  unixpid  5668  f0rn0  6088  f1ocnv  6147  tz6.12c  6211  funbrfv  6232  funopsn  6410  f1dom3el3dif  6523  oprabid  6674  oprabv  6700  ndmovordi  6822  elovmpt2rab  6877  elovmpt2rab1  6878  elovmpt3rab1  6890  limomss  7067  unielxp  7201  bropfvvvvlem  7253  f1o2ndf1  7282  smogt  7461  tfrlem1  7469  oawordeulem  7631  omass  7657  ecopovtrn  7847  php  8141  unxpdom  8164  findcard2d  8199  findcard3  8200  isfinite2  8215  fsuppimp  8278  fsuppunfi  8292  fsuppunbi  8293  fsuppres  8297  cantnfval2  8563  cantnfle  8565  cantnfp1lem3  8574  cantnflem1  8583  cnfcom  8594  rankr1ai  8658  rankonidlem  8688  rankxplim2  8740  oncard  8783  ficardom  8784  cardne  8788  acnnum  8872  alephord2i  8897  cardaleph  8909  aceq3lem  8940  dfac5lem5  8947  dfac12lem3  8964  cdainf  9011  ackbij1lem16  9054  cfslb  9085  cfslb2n  9087  cfsmolem  9089  fin4i  9117  infpssr  9127  fin1a2lem6  9224  axdc3lem2  9270  axcclem  9276  ttukeylem6  9333  fodomb  9345  gchi  9443  fpwwe2lem5  9453  pwfseqlem4  9481  pwfseq  9483  inawina  9509  wunfi  9540  inar1  9594  ltexnq  9794  ltbtwnnq  9797  ltexprlem4  9858  ltexpri  9862  prlem936  9866  suplem1pr  9871  suplem2pr  9872  recexsrlem  9921  mulgt0sr  9923  map2psrpr  9928  supsr  9930  eqlei  10144  eqlei2  10145  ledivp1i  10946  nnind  11035  nnmulcl  11040  nn0ge2m1nn  11357  nnnegz  11377  ublbneg  11770  xmulasslem  12112  ixxssixx  12186  iccshftri  12304  iccshftli  12306  iccdili  12308  icccntri  12310  fzo1fzo0n0  12514  elfzonlteqm1  12539  elfzo0l  12554  ssfzo12  12557  elfzo1elm1fzo0  12565  elfzr  12576  elfzlmr  12577  zmodidfzoimp  12695  mptnn0fsuppr  12794  seqp1  12811  seqcl2  12814  seqfveq2  12818  seqshft2  12822  monoord  12826  seqsplit  12829  seqcaopr3  12831  seqf1olem2a  12834  seqf1o  12837  seqid2  12842  seqhomo  12843  hashf1rn  13137  hashf1rnOLD  13138  hashinfxadd  13169  hashf1lem2  13235  seqcoll  13243  hash2pr  13246  pr2pwpr  13256  hashge2el2difr  13258  hash3tr  13267  fi1uzind  13274  brfi1indALT  13277  fi1uzindOLD  13280  brfi1indALTOLD  13283  elovmptnn0wrd  13343  swrdswrd  13454  swrdccatin12lem2a  13479  swrdccat  13487  swrdccatin1d  13493  swrdccatin2d  13494  swrdccatin12d  13495  repswccat  13526  cshwidxmod  13543  relexpsucnnr  13759  rtrclreclem3  13794  rtrclreclem4  13795  dfrtrcl2  13796  relexpindlem  13797  relexpind  13798  rtrclind  13799  cjre  13873  climeu  14280  climub  14386  fsum2d  14496  fsumabs  14527  fsumrlim  14537  fsumo1  14538  fsumiun  14547  prodfn0  14620  prodfrec  14621  ntrivcvg  14623  fprodabs  14698  fprod2d  14705  fprodefsum  14819  ruclem9  14961  dvdsabseq  15029  mod2eq1n2dvds  15065  mulsucdiv2z  15071  nno  15092  nn0o  15093  sadcadd  15174  sadadd2  15176  saddisjlem  15180  smuval2  15198  smupval  15204  smueqlem  15206  smumullem  15208  dfgcd2  15257  lcmgcdlem  15313  lcmftp  15343  exprmfct  15410  eulerthlem2  15481  dvdsprmpweqnn  15583  dvdsprmpweqle  15584  pcmpt  15590  vdwlem10  15688  cshwsidrepsw  15794  cshwshashlem1  15796  prmlem1a  15807  setsn0fun  15889  ressval3d  15931  mreexexd  16302  mreexexdOLD  16303  letsr  17221  ghmghmrn  17673  pmtrfrn  17872  pmtr3ncom  17889  gsmtrcl  17930  psgnsn  17934  sylow1lem1  18007  efginvrel2  18134  efgsrel  18141  cntzcmnss  18240  gsumzoppg  18338  gsum2dlem2  18364  telgsumfzs  18380  dprdval  18396  ablfac1eulem  18465  pgpfac1  18473  pgpfac  18477  srgpcomp  18526  ring1ne0  18585  rimf1o  18728  rimrhm  18729  brric2  18739  0ringnnzr  19263  mplcoe1  19459  mplcoe3  19460  mplcoe5lem  19461  mplcoe5  19462  mpfaddcl  19528  mpfmulcl  19529  coe1ae0  19580  coe1fzgsumd  19666  gsummoncoe1  19668  pf1addcl  19711  pf1mulcl  19712  evl1gsumd  19715  zrhpsgnelbas  19934  psgndiflemA  19941  mamufacex  20189  mat0dimcrng  20270  mavmulsolcl  20351  mdetunilem9  20420  cramerlem3  20489  pmatcollpw3fi1  20587  pm2mpfo  20613  chmaidscmat  20647  chfacfscmul0  20657  chfacfpmmul0  20661  cpmadugsumlemF  20675  tg2  20763  neindisj2  20921  neiptopnei  20930  t1t0  21146  fiuncmp  21201  hmeof1o  21561  ist1-5lem  21617  t1r0  21618  alexsublem  21842  imasdsf1olem  22172  tgioo  22593  fsumcn  22667  voliunlem3  23314  itgfsum  23587  dvbsss  23660  dvmptfsum  23732  dvfsumlem2  23784  dvfsumlem4  23786  plyco  23991  dgrcolem1  24023  dgrco  24025  dvntaylp  24119  taylthlem1  24121  jensen  24709  bposlem5  25007  lgsqrmodndvds  25072  gausslemma2dlem0i  25083  gausslemma2dlem4  25088  lgsquad2lem2  25104  2lgslem3  25123  2lgs  25126  2lgsoddprm  25135  dchrisum0flb  25193  pntpbnd1  25269  pntlemf  25288  brbtwn  25773  brcgr  25774  umgrnloopv  25995  umgrnloop  25997  usgrnloopvALT  26087  usgrnloopALT  26089  usgredg2vlem2  26112  subgrprop  26159  uvtxaisvtx  26283  vtxnbuvtx  26285  uvtxanbgrvtx  26287  cusgrsize2inds  26343  rgrprop  26450  rusgrprop  26452  wlkprop  26501  wlkvtxeledg  26513  wlkeq  26523  wlkl1loop  26528  wlk1walk  26529  uspgr2wlkeqi  26538  wlkreslem  26560  wlkres  26561  redwlk  26563  lfgrwlknloop  26580  2pthnloop  26621  usgr2trlncl  26650  usgr2pth  26654  clwlkcompim  26670  uspgrn2crct  26694  crctcshwlkn0  26707  wwlknp  26728  wwlkswwlksn  26744  wlkiswwlks2lem4  26752  wlkiswwlks2  26755  wlklnwwlkln2lem  26762  wwlksnext  26782  wwlksnextbi  26783  wwlksnredwwlkn0  26785  wwlksnextwrd  26786  clwwlknp  26881  clwwlkclwwlkn  26885  clwlkclwwlklem2a  26893  clwlkclwwlklem2  26895  clwwlksext2edg  26916  clwwisshclwws  26921  clwwnisshclwwsn  26923  umgrhashecclwwlk  26948  clwwlksnun  26967  1pthond  26997  upgr3v3e3cycl  27033  upgr4cycl4dv4e  27038  eupth2  27092  3vfriswmgr  27135  3cyclfrgrrn1  27142  n4cyclfrgr  27148  frgrnbnb  27150  frgrncvvdeqlem3  27158  frgrncvvdeqlem6  27161  frgrncvvdeqlem7  27162  frgrncvvdeqlem8  27163  frgrwopreglem4  27170  frgrwopreg  27172  frgrregorufr0  27175  frgr2wwlkeqm  27182  numclwwlk8  27234  frgrreggt1  27235  frgrregord013  27237  frgrregord13  27238  frgrogt3nreg  27239  friendshipgt3  27240  friendship  27241  blocn2  27647  cvexchlem  29211  cdj3lem2b  29280  cnvoprab  29483  nnindf  29550  issgon  30171  sitgclg  30389  sseqp1  30442  bnj938  30992  bnj964  30998  bnj1052  31028  bnj1125  31045  subfacp1lem6  31152  cvmliftlem7  31258  cvmliftlem10  31261  mclsrcl  31443  pprodss4v  31975  segleantisym  32206  rankeq1o  32262  bj-restv  33032  iooelexlt  33190  relowlssretop  33191  rdgeqoa  33198  matunitlindflem1  33385  poimirlem22  33411  poimirlem25  33414  poimirlem28  33417  poimirlem31  33420  mblfinlem3  33428  mbfresfi  33436  mettrifi  33533  opidon2OLD  33633  isexid2  33634  grpomndo  33654  elghomlem2OLD  33665  rngoidmlem  33715  rngoueqz  33719  iscringd  33777  cdlemk35s  36051  cdlemk39s  36053  cdlemk42  36055  mzpadd  37127  mzpmul  37128  mzpcompact2  37141  dford3lem2  37420  aomclem6  37455  cnsrexpcl  37561  relexpss1d  37823  iunrelexpmin1  37826  iunrelexpmin2  37830  nzin  38343  axc11next  38433  iotavalsb  38460  ssdec  39091  fperiodmullem  39336  fmul01  39618  fmulcl  39619  fmuldfeqlem1  39620  fmuldfeq  39621  fprodcnlem  39637  iblspltprt  39958  itgspltprt  39964  stoweidlem2  39988  stoweidlem3  39989  stoweidlem6  39992  stoweidlem8  39994  stoweidlem17  40003  stoweidlem19  40005  stoweidlem21  40007  stoweidlem26  40012  stoweidlem31  40017  stoweidlem43  40029  fourierdlem42  40135  eu2ndop1stv  40971  funressnfv  40977  afv0fv0  40998  afv0nbfvbi  41000  nelbrim  41061  ssfz12  41093  fzoopth  41106  smonoord  41111  iccpartiltu  41128  iccpartigtl  41129  iccelpart  41139  icceuelpart  41142  fargshiftf  41146  fargshiftf1  41147  fargshiftfo  41148  lighneallem4  41298  mogoldbblem  41400  sbgoldbwt  41436  bgoldbtbndlem2  41465  bgoldbtbndlem4  41467  tgoldbach  41476  tgoldbachOLD  41483  upwlkwlk  41491  sprel  41505  sprsymrelf1lem  41512  sprsymrelfolem2  41514  clcllaw  41598  intop  41610  clintop  41615  assintop  41616  assintopcllaw  41619  lmod0rng  41639  ringrng  41650  rngimf1o  41676  rngimrnghm  41677  ztprmneprm  41896  scmsuppss  41924  ply1mulgsumlem1  41945  ply1mulgsumlem2  41946  lcoel0  41988  ellcoellss  41995  lindslinindsimp2lem5  42022  ldepspr  42033  flnn0div2ge  42098  nnolog2flm1  42155  blengt1fldiv2p1  42158  dignn0flhalf  42183
  Copyright terms: Public domain W3C validator