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

Theorem mpcom 36
Description: Modus ponens inference with commutation of antecedents. (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 31 . 2
41, 3mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  syldan  470  axc16i  2064  sbcn1  3375  sbcim1  3376  sbcbi1  3377  sbcel21v  3395  elimasni  5369  sotri  5399  sotriOLD  5404  relcoi1  5541  unixpid  5547  f0rn0  5775  f1ocnv  5833  tz6.12c  5890  funbrfv  5911  f1dom3el3dif  6176  oprabid  6323  oprabv  6345  ndmovordi  6466  elovmpt2rab  6521  elovmpt2rab1  6522  elovmpt3rab1  6536  limomss  6705  unielxp  6836  f1o2ndf1  6908  smogt  7057  tfrlem1  7064  oawordeulem  7222  omass  7248  ecopovtrn  7433  php  7721  unxpdom  7747  findcard2d  7782  findcard3  7783  isfinite2  7798  fsuppimp  7855  fsuppunfi  7869  fsuppunbi  7870  fsuppres  7874  cantnfval2  8109  cantnfle  8111  cantnfp1lem3  8120  cantnflem1  8129  cantnfval2OLD  8139  cantnfleOLD  8141  cantnfp1lem3OLD  8146  cantnflem1OLD  8152  cnfcom  8165  cnfcomOLD  8173  rankr1ai  8237  rankonidlem  8267  rankxplim2  8319  oncard  8362  ficardom  8363  cardne  8367  acnnum  8454  alephord2i  8479  cardaleph  8491  aceq3lem  8522  dfac5lem5  8529  dfac12lem3  8546  cdainf  8593  ackbij1lem16  8636  cfslb  8667  cfslb2n  8669  cfsmolem  8671  fin4i  8699  infpssr  8709  fin1a2lem6  8806  axdc3lem2  8852  axcclem  8858  ttukeylem6  8915  fodomb  8925  gchi  9023  fpwwe2lem5  9033  pwfseqlem4  9061  pwfseq  9063  inawina  9089  wunfi  9120  inar1  9174  ltexnq  9374  ltbtwnnq  9377  ltexprlem4  9438  ltexpri  9442  prlem936  9446  suplem1pr  9451  suplem2pr  9452  recexsrlem  9501  mulgt0sr  9503  map2psrpr  9508  supsr  9510  eqlei  9715  eqlei2  9716  ledivp1i  10496  nnind  10579  nnmulcl  10584  nn0ge2m1nn  10886  nnnegz  10892  uzindOLD  10982  ublbneg  11195  xmulasslem  11506  ixxssixx  11572  iccshftri  11684  iccshftli  11686  iccdili  11688  icccntri  11690  1fv  11821  fzo1fzo0n0  11864  elfzonlteqm1  11891  ssfzo12  11905  zmodidfzoimp  12026  mptnn0fsuppr  12105  seqp1  12122  seqcl2  12125  seqfveq2  12129  seqshft2  12133  monoord  12137  seqsplit  12140  seqcaopr3  12142  seqf1olem2a  12145  seqf1o  12148  seqid2  12153  seqhomo  12154  hashf1rn  12425  hashinfxadd  12453  hashle00  12465  hashf1lem2  12505  seqcoll  12512  hash2pr  12515  pr2pwpr  12520  hash3tr  12529  brfi1uzind  12532  snopiswrd  12556  elovmptnn0wrd  12584  swrdswrd  12685  swrdccatin12lem2a  12710  swrdccat  12718  swrdccatin1d  12724  swrdccatin2d  12725  swrdccatin12d  12726  repswccat  12757  cshwidxmod  12774  cjre  12972  climeu  13378  climub  13484  fsum2d  13586  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  prodfn0  13703  prodfrec  13704  ntrivcvg  13706  fprodabs  13778  fprod2d  13785  fprodefsum  13830  ruclem9  13971  sadcadd  14108  sadadd2  14110  saddisjlem  14114  smuval2  14132  smupval  14138  smueqlem  14140  smumullem  14142  exprmfct  14251  eulerthlem2  14312  pcmpt  14411  vdwlem10  14508  cshwsidrepsw  14578  cshwshashlem1  14580  prmlem1a  14592  mreexexd  15045  letsr  15857  pmtrfrn  16483  pmtr3ncom  16500  gsmtrcl  16541  psgnsn  16545  sylow1lem1  16618  efginvrel2  16745  efgsrel  16752  cntzcmnss  16849  gsumzoppg  16967  gsum2dlem2  16998  gsum2dOLD  17000  telgsumfzs  17018  dprdval  17034  dprdvalOLD  17036  ablfac1eulem  17123  pgpfac1  17131  pgpfac  17135  srgpcomp  17183  ring1ne0  17239  rimf1o  17383  rimrhm  17384  brric2  17394  0ringnnzr  17917  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5lem  18130  mplcoe5  18131  mplcoe2OLD  18133  mpfaddcl  18203  mpfmulcl  18204  coe1ae0  18257  coe1fzgsumd  18344  gsummoncoe1  18346  pf1addcl  18389  pf1mulcl  18390  evl1gsumd  18393  zrhpsgnelbas  18630  psgndiflemA  18637  mamufacex  18891  mat0dimcrng  18972  mavmulsolcl  19053  mdetunilem9  19122  cramerlem3  19191  pmatcollpw3fi1  19289  pm2mpfo  19315  chmaidscmat  19349  chfacfscmul0  19359  chfacfpmmul0  19363  cpmadugsumlemF  19377  tg2  19466  neindisj2  19624  neiptopnei  19633  t1t0  19849  fiuncmp  19904  bwthOLD  19911  hmeof1o  20265  ist1-5lem  20321  t1r0  20322  alexsublem  20544  imasdsf1olem  20876  tgioo  21301  fsumcn  21374  voliunlem3  21962  itgfsum  22233  dvbsss  22306  dvmptfsum  22376  dvfsumlem2  22428  dvfsumlem4  22430  plyco  22638  dgrcolem1  22670  dgrco  22672  dvntaylp  22766  taylthlem1  22768  jensen  23318  bposlem5  23563  lgsquad2lem2  23634  dchrisum0flb  23695  pntpbnd1  23771  pntlemf  23790  brbtwn  24202  brcgr  24203  ushgrauhgra  24303  uhgra0v  24310  umisuhgra  24327  usgrac  24351  uslgraf1oedg  24359  uslisushgra  24363  uslisumgra  24364  usisuslgra  24365  elusuhgra  24368  usgra0v  24371  usgranloopv  24378  usgranloop  24379  usgra1v  24390  usgraidx2vlem2  24392  usgrafisindb0  24408  usgrafisindb1  24409  usgrafisinds  24413  usgrafisbase  24414  iscusgra0  24457  cusgrasize2inds  24477  cusgrafi  24482  2mwlk  24521  iswlkg  24524  wlkcpr  24529  edgwlk  24531  trliswlk  24541  2trllemE  24555  usgrnloop  24565  pthistrl  24574  spthispth  24575  pthdepisspth  24576  redwlk  24608  wlkdvspth  24610  usgra2adedgspthlem2  24612  usgra2wlkspth  24621  crctistrl  24628  cyclispth  24629  cycliscrct  24630  cyclnspth  24631  cyclispthon  24633  fargshiftf  24636  fargshiftf1  24637  fargshiftfo  24638  usgrcyclnl1  24640  usgrcyclnl2  24641  nvnencycllem  24643  3v3e3cycl1  24644  constr3trllem5  24654  constr3trl  24659  constr3pth  24660  constr3cycl  24661  4cycl4v4e  24666  4cycl4dv4e  24668  cusconngra  24676  wwlknimp  24687  wwlkn0  24689  wlkiswwlk1  24690  wlkiswwlk2lem4  24694  wlkiswwlk2  24697  wlklniswwlkn2  24700  wwlkiswwlkn  24702  2wlkeq  24707  wwlknred  24723  wwlknext  24724  wwlknextbi  24725  wwlknredwwlkn0  24727  wwlkextwrd  24728  wwlkm1edg  24735  wwlkextproplem3  24743  isclwlkg  24755  clwlkswlks  24758  clwwlkprop  24770  clwwlkgt0  24771  clwwlknimp  24776  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkext2edg  24802  clwwisshclww  24807  clwwnisshclwwn  24809  usghashecclwwlk  24835  wlklenvclwlk  24839  2spontn0vne  24887  usg2spthonot  24888  usg2spthonot0  24889  usgfidegfi  24910  usgravd00  24919  rgraprop  24928  rusgraprop  24929  rusgrargra  24930  cusgraisrusgra  24938  0eusgraiff0rgracl  24941  rusgrasn  24945  rusgranumwlklem1  24949  eupatrl  24968  eupath2  24980  3vfriswmgra  25005  3cyclfrgrarn1  25012  3cyclfrgrarn  25013  n4cyclfrgra  25018  frgranbnb  25020  frconngra  25021  vdfrgra0  25022  vdn0frgrav2  25023  vdgn0frgrav2  25024  usgn0fidegnn0  25029  frgrancvvdeqlem4  25033  frgrancvvdeqlem7  25036  frgrancvvdeqlemA  25037  frgrancvvdeqlemB  25038  frgrawopreglem4  25047  frgrawopreglem5  25048  frgrawopreg  25049  frgraregorufr0  25052  frgraeu  25054  frg2wot1  25057  frg2woteqm  25059  frg2woteq  25060  frgregordn0  25070  numclwwlkun  25079  numclwwlk8  25115  frgrareggt1  25116  frgrareg  25117  frgraregord013  25118  frgraregord13  25119  frgraogt3nreg  25120  friendshipgt3  25121  friendship  25122  opidon2OLD  25326  isexid2  25327  grpomndo  25348  elghomlem2OLD  25364  rngoidmlem  25425  rngoueqz  25432  blocn2  25723  cvexchlem  27287  cdj3lem2b  27356  cnvoprab  27546  nnindf  27610  issgon  28123  sitgclg  28284  sseqp1  28334  subfacp1lem6  28629  cvmliftlem7  28736  cvmliftlem10  28739  mclsrcl  28921  relexp0  29052  relexpsucr  29053  relexpsucl  29055  relexprel  29057  relexpdm  29058  relexprn  29059  relexpadd  29061  relexpindlem  29062  relexpind  29063  rtrclreclem.trans  29069  rtrclreclem.min  29070  dfrtrcl2  29071  rtrclind  29072  pprodss4v  29534  segleantisym  29765  rankeq1o  29828  mblfinlem3  30053  mbfresfi  30061  mettrifi  30250  iscringd  30396  mzpadd  30670  mzpmul  30671  mzpcompact2  30685  dford3lem2  30969  aomclem6  31005  cnsrexpcl  31114  lcmgcdlem  31212  nzin  31223  axc11next  31313  iotavalsb  31340  fperiodmullem  31503  fmul01  31574  fmulcl  31575  fmuldfeqlem1  31576  fmuldfeq  31577  iblspltprt  31772  itgspltprt  31778  stoweidlem2  31784  stoweidlem3  31785  stoweidlem6  31788  stoweidlem8  31790  stoweidlem17  31799  stoweidlem19  31801  stoweidlem21  31803  stoweidlem26  31808  stoweidlem31  31813  stoweidlem43  31825  fourierdlem42  31931  eu2ndop1stv  32207  funressnfv  32213  afv0fv0  32234  afv0nbfvbi  32236  ssfz12  32330  fzoopth  32340  usgra2pthspth  32351  spthdifv  32352  usgra2pth  32354  uhgrasiz  32394  usgfis  32446  usgfisALT  32450  clcllaw  32515  intop  32527  clintop  32532  assintop  32533  assintopcllaw  32536  ressval3d  32558  lmod0rng  32674  ringrng  32685  rngimf1o  32711  rngimrnghm  32712  ztprmneprm  32936  scmsuppss  32965  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  lcoel0  33029  ellcoellss  33036  lindslinindsimp2lem5  33063  ldepspr  33074  bnj938  33995  bnj964  34001  bnj1052  34031  bnj1125  34048  cdlemk35s  36663  cdlemk39s  36665  cdlemk42  36667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator