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  486  axc16i  2353  sbcn1  3514  sbcim1  3515  sbcbi1  3516  sbcel21v  3530  elimasni  5527  sotri  5558  unixpid  5708  f0rn0  6128  f1ocnv  6187  tz6.12c  6251  funbrfv  6272  funopsn  6453  f1dom3el3dif  6566  oprabid  6717  oprabv  6745  ndmovordi  6867  elovmpt2rab  6922  elovmpt2rab1  6923  elovmpt3rab1  6935  limomss  7112  unielxp  7248  bropfvvvvlem  7301  f1o2ndf1  7330  smogt  7509  tfrlem1  7517  oawordeulem  7679  omass  7705  ecopovtrn  7893  php  8185  unxpdom  8208  findcard2d  8243  findcard3  8244  isfinite2  8259  fsuppimp  8322  fsuppunfi  8336  fsuppunbi  8337  fsuppres  8341  cantnfval2  8604  cantnfle  8606  cantnfp1lem3  8615  cantnflem1  8624  cnfcom  8635  rankr1ai  8699  rankonidlem  8729  rankxplim2  8781  oncard  8824  ficardom  8825  cardne  8829  acnnum  8913  alephord2i  8938  cardaleph  8950  aceq3lem  8981  dfac5lem5  8988  dfac12lem3  9005  cdainf  9052  ackbij1lem16  9095  cfslb  9126  cfslb2n  9128  cfsmolem  9130  fin4i  9158  infpssr  9168  fin1a2lem6  9265  axdc3lem2  9311  axcclem  9317  ttukeylem6  9374  fodomb  9386  gchi  9484  fpwwe2lem5  9494  pwfseqlem4  9522  pwfseq  9524  inawina  9550  wunfi  9581  inar1  9635  ltexnq  9835  ltbtwnnq  9838  ltexprlem4  9899  ltexpri  9903  prlem936  9907  suplem1pr  9912  suplem2pr  9913  recexsrlem  9962  mulgt0sr  9964  map2psrpr  9969  supsr  9971  eqlei  10185  eqlei2  10186  ledivp1i  10987  nnind  11076  nnmulcl  11081  nn0ge2m1nn  11398  nnnegz  11418  ublbneg  11811  xmulasslem  12153  ixxssixx  12227  iccshftri  12345  iccshftli  12347  iccdili  12349  icccntri  12351  elfz1b  12447  fzo1fzo0n0  12558  elfzonlteqm1  12583  elfzo0l  12598  ssfzo12  12601  elfzo1elm1fzo0  12609  elfzr  12621  elfzlmr  12622  zmodidfzoimp  12740  mptnn0fsuppr  12839  seqp1  12856  seqcl2  12859  seqfveq2  12863  seqshft2  12867  monoord  12871  seqsplit  12874  seqcaopr3  12876  seqf1olem2a  12879  seqf1o  12882  seqid2  12887  seqhomo  12888  hashf1rn  13181  hashinfxadd  13212  hashf1lem2  13278  seqcoll  13286  hash2pr  13289  pr2pwpr  13299  hashge2el2difr  13301  hash3tr  13310  fi1uzind  13317  brfi1indALT  13320  elovmptnn0wrd  13381  swrdswrd  13506  swrdccatin12lem2a  13531  swrdccat  13539  swrdccatin1d  13545  swrdccatin2d  13546  swrdccatin12d  13547  repswccat  13578  cshwidxmod  13595  relexpsucnnr  13809  rtrclreclem3  13844  rtrclreclem4  13845  dfrtrcl2  13846  relexpindlem  13847  relexpind  13848  rtrclind  13849  cjre  13923  climeu  14330  climub  14436  fsum2d  14546  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fsumiun  14597  prodfn0  14670  prodfrec  14671  ntrivcvg  14673  fprodabs  14748  fprod2d  14755  fprodefsum  14869  ruclem9  15011  dvdsmod0  15033  p1modz1  15034  dvdsmodexp  15035  dvdsabseq  15082  mod2eq1n2dvds  15118  mulsucdiv2z  15124  nno  15145  nn0o  15146  sadcadd  15227  sadadd2  15229  saddisjlem  15233  smuval2  15251  smupval  15257  smueqlem  15259  smumullem  15261  dfgcd2  15310  lcmgcdlem  15366  lcmftp  15396  exprmfct  15463  eulerthlem2  15534  dvdsprmpweqnn  15636  dvdsprmpweqle  15637  pcmpt  15643  vdwlem10  15741  cshwsidrepsw  15847  cshwshashlem1  15849  prmlem1a  15860  setsn0fun  15942  ressval3d  15984  mreexexd  16355  mreexexdOLD  16356  letsr  17274  ghmghmrn  17726  pmtrfrn  17924  pmtr3ncom  17941  gsmtrcl  17982  psgnsn  17986  sylow1lem1  18059  efginvrel2  18186  efgsrel  18193  cntzcmnss  18292  gsumzoppg  18390  gsum2dlem2  18416  telgsumfzs  18432  dprdval  18448  ablfac1eulem  18517  pgpfac1  18525  pgpfac  18529  srgpcomp  18578  ring1ne0  18637  rimf1o  18782  rimrhm  18783  brric2  18793  0ringnnzr  19317  mplcoe1  19513  mplcoe3  19514  mplcoe5lem  19515  mplcoe5  19516  mpfaddcl  19582  mpfmulcl  19583  coe1ae0  19634  coe1fzgsumd  19720  gsummoncoe1  19722  pf1addcl  19765  pf1mulcl  19766  evl1gsumd  19769  zrhpsgnelbas  19988  psgndiflemA  19995  mamufacex  20243  mat0dimcrng  20324  mavmulsolcl  20405  mdetunilem9  20474  cramerlem3  20543  pmatcollpw3fi1  20641  pm2mpfo  20667  chmaidscmat  20701  chfacfscmul0  20711  chfacfpmmul0  20715  cpmadugsumlemF  20729  tg2  20817  neindisj2  20975  neiptopnei  20984  t1t0  21200  fiuncmp  21255  hmeof1o  21615  ist1-5lem  21671  t1r0  21672  alexsublem  21895  imasdsf1olem  22225  tgioo  22646  fsumcn  22720  voliunlem3  23366  itgfsum  23638  dvbsss  23711  dvmptfsum  23783  dvfsumlem2  23835  dvfsumlem4  23837  plyco  24042  dgrcolem1  24074  dgrco  24076  dvntaylp  24170  taylthlem1  24172  jensen  24760  bposlem5  25058  lgsqrmodndvds  25123  gausslemma2dlem0i  25134  gausslemma2dlem4  25139  lgsquad2lem2  25155  2lgslem3  25174  2lgs  25177  2lgsoddprm  25186  dchrisum0flb  25244  pntpbnd1  25320  pntlemf  25339  brbtwn  25824  brcgr  25825  umgrnloopv  26046  umgrnloop  26048  usgrnloopvALT  26138  usgrnloopALT  26140  usgredg2vlem2  26163  subgrprop  26210  uvtxnbgrvtx  26341  cusgrsize2inds  26405  rgrprop  26512  rusgrprop  26514  wlkprop  26563  wlkvtxeledg  26575  wlkeq  26585  wlkl1loop  26590  wlk1walk  26591  uspgr2wlkeqi  26600  wlkreslem  26622  wlkres  26623  redwlk  26625  lfgrwlknloop  26642  2pthnloop  26683  usgr2trlncl  26712  usgr2pth  26716  clwlkcompim  26732  uspgrn2crct  26756  crctcshwlkn0  26769  wwlknp  26791  wwlkswwlksn  26819  wlkiswwlks2lem4  26826  wlkiswwlks2  26829  wlklnwwlkln2lem  26836  wwlksnext  26856  wwlksnextbi  26857  wwlksnredwwlkn0  26859  wwlksnextwrd  26860  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwwisshclwws  26972  clwwlknp  26999  clwwlknwwlksn  27000  clwwlkwwlksb  27018  clwwlkext2edg  27020  umgrhashecclwwlk  27042  clwwlknun  27087  clwwlknunOLD  27091  1pthond  27122  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  eupth2  27217  3vfriswmgr  27258  3cyclfrgrrn1  27265  n4cyclfrgr  27271  frgrnbnb  27273  frgrncvvdeqlem3  27281  frgrncvvdeqlem6  27284  frgrncvvdeqlem7  27285  frgrncvvdeqlem8  27286  frgrwopreglem4a  27290  frgrwopreg  27303  frgrregorufr0  27304  frgr2wwlkeqm  27311  frgrreggt1  27380  frgrregord013  27382  frgrregord13  27383  frgrogt3nreg  27384  friendshipgt3  27385  friendship  27386  blocn2  27791  cvexchlem  29355  cdj3lem2b  29424  cnvoprabOLD  29626  nnindf  29693  issgon  30314  sitgclg  30532  sseqp1  30585  bnj938  31133  bnj964  31139  bnj1052  31169  bnj1125  31186  subfacp1lem6  31293  cvmliftlem7  31399  cvmliftlem10  31402  mclsrcl  31584  pprodss4v  32116  segleantisym  32347  rankeq1o  32403  bj-restv  33173  iooelexlt  33340  relowlssretop  33341  rdgeqoa  33348  matunitlindflem1  33535  poimirlem22  33561  poimirlem25  33564  poimirlem28  33567  poimirlem31  33570  mblfinlem3  33578  mbfresfi  33586  mettrifi  33683  opidon2OLD  33783  isexid2  33784  grpomndo  33804  elghomlem2OLD  33815  rngoidmlem  33865  rngoueqz  33869  iscringd  33927  cdlemk35s  36542  cdlemk39s  36544  cdlemk42  36546  mzpadd  37618  mzpmul  37619  mzpcompact2  37632  dford3lem2  37911  aomclem6  37946  cnsrexpcl  38052  relexpss1d  38314  iunrelexpmin1  38317  iunrelexpmin2  38321  nzin  38834  axc11next  38924  iotavalsb  38951  ssdec  39579  fperiodmullem  39831  monoordxrv  40025  fmul01  40130  fmulcl  40131  fmuldfeqlem1  40132  fmuldfeq  40133  fprodcnlem  40149  iblspltprt  40507  itgspltprt  40513  stoweidlem2  40537  stoweidlem3  40538  stoweidlem6  40541  stoweidlem8  40543  stoweidlem17  40552  stoweidlem19  40554  stoweidlem21  40556  stoweidlem26  40561  stoweidlem31  40566  stoweidlem43  40578  fourierdlem42  40684  eu2ndop1stv  41523  funressnfv  41529  afv0fv0  41550  afv0nbfvbi  41552  nelbrim  41616  ssfz12  41649  fzoopth  41662  smonoord  41666  iccpartiltu  41683  iccpartigtl  41684  iccelpart  41694  icceuelpart  41697  fargshiftf  41701  fargshiftf1  41702  fargshiftfo  41703  lighneallem4  41852  mogoldbblem  41954  sbgoldbwt  41990  bgoldbtbndlem2  42019  bgoldbtbndlem4  42021  tgoldbach  42030  tgoldbachOLD  42037  upwlkwlk  42045  sprel  42059  sprsymrelf1lem  42066  sprsymrelfolem2  42068  clcllaw  42152  intop  42164  clintop  42169  assintop  42170  assintopcllaw  42173  lmod0rng  42193  ringrng  42204  rngimf1o  42230  rngimrnghm  42231  ztprmneprm  42450  scmsuppss  42478  ply1mulgsumlem1  42499  ply1mulgsumlem2  42500  lcoel0  42542  ellcoellss  42549  lindslinindsimp2lem5  42576  ldepspr  42587  flnn0div2ge  42652  nnolog2flm1  42709  blengt1fldiv2p1  42712  dignn0flhalf  42737
  Copyright terms: Public domain W3C validator