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  571  axc16i  2471  sbcn1  3631  sbcim1  3632  sbcbi1  3633  sbcel21v  3646  elimasni  5633  sotri  5664  unixpid  5814  f0rn0  6230  f1ocnv  6290  tz6.12c  6354  funbrfv  6375  f1dom3el3dif  6668  oprabid  6821  oprabv  6849  ndmovordi  6971  elovmpt2rab  7026  elovmpt2rab1  7027  elovmpt3rab1  7039  limomss  7216  unielxp  7352  bropfvvvvlem  7406  f1o2ndf1  7435  smogt  7616  tfrlem1  7624  oawordeulem  7787  omass  7813  ecopovtrn  8002  php  8299  unxpdom  8322  findcard2d  8357  findcard3  8358  isfinite2  8373  fsuppimp  8436  fsuppunfi  8450  fsuppunbi  8451  fsuppres  8455  cantnfval2  8729  cantnfle  8731  cantnfp1lem3  8740  cantnflem1  8749  cnfcom  8760  rankr1ai  8824  rankonidlem  8854  rankxplim2  8906  oncard  8985  ficardom  8986  cardne  8990  acnnum  9074  alephord2i  9099  cardaleph  9111  aceq3lem  9142  dfac5lem5  9149  dfac12lem3  9168  cdainf  9215  ackbij1lem16  9258  cfslb  9289  cfslb2n  9291  cfsmolem  9293  fin4i  9321  infpssr  9331  fin1a2lem6  9428  axdc3lem2  9474  axcclem  9480  ttukeylem6  9537  fodomb  9549  gchi  9647  fpwwe2lem5  9657  pwfseqlem4  9685  pwfseq  9687  inawina  9713  wunfi  9744  inar1  9798  ltexnq  9998  ltbtwnnq  10001  ltexprlem4  10062  ltexpri  10066  prlem936  10070  suplem1pr  10075  suplem2pr  10076  recexsrlem  10125  mulgt0sr  10127  map2psrpr  10132  supsr  10134  eqlei  10348  eqlei2  10349  ledivp1i  11150  nnind  11239  nnmulcl  11244  nn0ge2m1nn  11561  nnnegz  11581  ublbneg  11975  xmulasslem  12319  ixxssixx  12393  iccshftri  12513  iccshftli  12515  iccdili  12517  icccntri  12519  elfz1b  12615  fzo1fzo0n0  12726  elfzonlteqm1  12751  elfzo0l  12765  ssfzo12  12768  elfzo1elm1fzo0  12776  elfzr  12788  elfzlmr  12789  zmodidfzoimp  12907  mptnn0fsuppr  13005  seqp1  13022  seqcl2  13025  seqfveq2  13029  seqshft2  13033  monoord  13037  seqsplit  13040  seqcaopr3  13042  seqf1olem2a  13045  seqf1o  13048  seqid2  13053  seqhomo  13054  hashf1rn  13344  hashinfxadd  13375  hashf1lem2  13441  seqcoll  13449  hash2pr  13452  pr2pwpr  13462  hashge2el2difr  13464  hash3tr  13473  fi1uzind  13480  brfi1indALT  13483  elovmptnn0wrd  13544  swrdswrd  13668  swrdccatin12lem2a  13693  swrdccat  13701  swrdccatin1d  13707  swrdccatin2d  13708  swrdccatin12d  13709  repswccat  13740  cshwidxmod  13757  relexpsucnnr  13972  rtrclreclem3  14007  rtrclreclem4  14008  dfrtrcl2  14009  relexpindlem  14010  relexpind  14011  rtrclind  14012  cjre  14086  climeu  14493  climub  14599  fsum2d  14709  fsumabs  14739  fsumrlim  14749  fsumo1  14750  fsumiun  14759  prodfn0  14832  prodfrec  14833  ntrivcvg  14835  fprodabs  14910  fprod2d  14917  fprodefsum  15030  ruclem9  15172  dvdsmod0  15194  p1modz1  15195  dvdsmodexp  15196  dvdsabseq  15243  mod2eq1n2dvds  15278  mulsucdiv2z  15284  nno  15305  nn0o  15306  sadcadd  15387  sadadd2  15389  saddisjlem  15393  smuval2  15411  smupval  15417  smueqlem  15419  smumullem  15421  dfgcd2  15470  lcmgcdlem  15526  lcmftp  15556  exprmfct  15622  eulerthlem2  15693  dvdsprmpweqnn  15795  dvdsprmpweqle  15796  pcmpt  15802  vdwlem10  15900  cshwsidrepsw  16006  cshwshashlem1  16008  prmlem1a  16019  setsn0fun  16101  ressval3d  16143  ressval3dOLD  16144  mreexexd  16515  letsr  17434  ghmghmrn  17886  pmtrfrn  18084  pmtr3ncom  18101  gsmtrcl  18142  psgnsn  18146  sylow1lem1  18219  efginvrel2  18346  efgsrel  18353  cntzcmnss  18452  gsumzoppg  18550  gsum2dlem2  18576  telgsumfzs  18593  dprdval  18609  ablfac1eulem  18678  pgpfac1  18686  pgpfac  18690  srgpcomp  18739  ring1ne0  18798  rimf1o  18943  rimrhm  18944  brric2  18954  0ringnnzr  19483  mplcoe1  19679  mplcoe3  19680  mplcoe5lem  19681  mplcoe5  19682  mpfaddcl  19748  mpfmulcl  19749  coe1ae0  19800  coe1fzgsumd  19886  gsummoncoe1  19888  pf1addcl  19931  pf1mulcl  19932  evl1gsumd  19935  zrhpsgnelbas  20155  psgndiflemA  20162  mamufacex  20411  mat0dimcrng  20493  mavmulsolcl  20574  mdetunilem9  20643  cramerlem3  20714  pmatcollpw3fi1  20812  pm2mpfo  20838  chmaidscmat  20872  chfacfscmul0  20882  chfacfpmmul0  20886  cpmadugsumlemF  20900  tg2  20989  neindisj2  21147  neiptopnei  21156  t1t0  21372  fiuncmp  21427  hmeof1o  21787  ist1-5lem  21843  t1r0  21844  alexsublem  22067  imasdsf1olem  22397  tgioo  22818  fsumcn  22892  voliunlem3  23539  itgfsum  23812  dvbsss  23885  dvmptfsum  23957  dvfsumlem2  24009  dvfsumlem4  24011  plyco  24216  dgrcolem1  24248  dgrco  24250  dvntaylp  24344  taylthlem1  24346  jensen  24935  bposlem5  25233  lgsqrmodndvds  25298  gausslemma2dlem0i  25309  gausslemma2dlem4  25314  lgsquad2lem2  25330  2lgslem3  25349  2lgs  25352  2lgsoddprm  25361  dchrisum0flb  25419  pntpbnd1  25495  pntlemf  25514  brbtwn  25999  brcgr  26000  umgrnloopv  26221  umgrnloop  26223  usgrnloopvALT  26314  usgrnloopALT  26316  usgredg2vlem2  26339  subgrprop  26387  uvtxnbgrvtx  26519  cusgrsize2inds  26583  rgrprop  26690  rusgrprop  26692  wlkprop  26741  wlkvtxeledg  26753  wlkeq  26763  wlkl1loop  26768  wlk1walk  26769  uspgr2wlkeqi  26778  wlkreslem  26800  wlkres  26801  redwlk  26803  lfgrwlknloop  26820  2pthnloop  26861  usgr2trlncl  26890  usgr2pth  26894  clwlkcompim  26910  clwlkcompbp  26912  uspgrn2crct  26935  crctcshwlkn0  26948  wwlknp  26970  wwlkswwlksn  26998  wlkiswwlks2lem4  27005  wlkiswwlks2  27008  wlklnwwlkln2lem  27015  wwlksnext  27035  wwlksnextbi  27036  wwlksnredwwlkn0  27038  wwlksnextwrd  27039  clwlkclwwlklem2a  27145  clwlkclwwlklem2  27147  clwlkclwwlkflem  27151  clwwisshclwws  27162  clwwlknp  27189  clwwlknwwlksn  27190  clwwlkwwlksb  27208  clwwlkext2edg  27210  umgrhashecclwwlk  27233  clwwlknun  27285  clwwlknunOLD  27290  1pthond  27321  upgr3v3e3cycl  27357  upgr4cycl4dv4e  27362  eupth2  27416  3vfriswmgr  27457  3cyclfrgrrn1  27464  n4cyclfrgr  27470  frgrnbnb  27472  frgrncvvdeqlem3  27480  frgrncvvdeqlem6  27483  frgrncvvdeqlem7  27484  frgrncvvdeqlem8  27485  frgrwopreglem4a  27489  frgrwopreg  27502  frgrregorufr0  27503  frgr2wwlkeqm  27510  2clwwlk2clwwlklem  27528  wlkl0  27553  frgrreggt1  27586  frgrregord013  27588  frgrregord13  27589  frgrogt3nreg  27590  friendshipgt3  27591  friendship  27592  blocn2  27997  cvexchlem  29561  cdj3lem2b  29630  cnvoprabOLD  29832  nnindf  29899  issgon  30520  sitgclg  30738  sseqp1  30791  bnj938  31339  bnj964  31345  bnj1052  31375  bnj1125  31392  subfacp1lem6  31499  cvmliftlem7  31605  cvmliftlem10  31608  mclsrcl  31790  pprodss4v  32322  segleantisym  32553  rankeq1o  32609  bj-restv  33373  iooelexlt  33540  relowlssretop  33541  rdgeqoa  33548  matunitlindflem1  33731  poimirlem22  33757  poimirlem25  33760  poimirlem28  33763  poimirlem31  33766  mblfinlem3  33774  mbfresfi  33781  mettrifi  33878  opidon2OLD  33978  isexid2  33979  grpomndo  33999  elghomlem2OLD  34010  rngoidmlem  34060  rngoueqz  34064  iscringd  34122  cdlemk35s  36739  cdlemk39s  36741  cdlemk42  36743  mzpadd  37820  mzpmul  37821  mzpcompact2  37834  dford3lem2  38113  aomclem6  38148  cnsrexpcl  38254  relexpss1d  38516  iunrelexpmin1  38519  iunrelexpmin2  38523  nzin  39036  axc11next  39126  iotavalsb  39153  ssdec  39780  fperiodmullem  40028  monoordxrv  40222  fmul01  40324  fmulcl  40325  fmuldfeqlem1  40326  fmuldfeq  40327  fprodcnlem  40343  iblspltprt  40700  itgspltprt  40706  stoweidlem2  40730  stoweidlem3  40731  stoweidlem6  40734  stoweidlem8  40736  stoweidlem17  40745  stoweidlem19  40747  stoweidlem21  40749  stoweidlem26  40754  stoweidlem31  40759  stoweidlem43  40771  fourierdlem42  40877  eu2ndop1stv  41716  funressnfv  41722  afv0fv0  41743  afv0nbfvbi  41745  nelbrim  41809  ssfz12  41842  fzoopth  41855  smonoord  41859  iccpartiltu  41876  iccpartigtl  41877  iccelpart  41887  icceuelpart  41890  fargshiftf  41894  fargshiftf1  41895  fargshiftfo  41896  lighneallem4  42045  mogoldbblem  42147  sbgoldbwt  42183  bgoldbtbndlem2  42212  bgoldbtbndlem4  42214  tgoldbach  42223  tgoldbachOLD  42230  upwlkwlk  42238  sprel  42252  sprsymrelf1lem  42259  sprsymrelfolem2  42261  clcllaw  42345  intop  42357  clintop  42362  assintop  42363  assintopcllaw  42366  lmod0rng  42386  ringrng  42397  rngimf1o  42423  rngimrnghm  42424  ztprmneprm  42643  scmsuppss  42671  ply1mulgsumlem1  42692  ply1mulgsumlem2  42693  lcoel0  42735  ellcoellss  42742  lindslinindsimp2lem5  42769  ldepspr  42780  flnn0div2ge  42845  nnolog2flm1  42902  blengt1fldiv2p1  42905  dignn0flhalf  42930
  Copyright terms: Public domain W3C validator