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

Theorem a2d 26
Description: Deduction distributing an embedded antecedent. Deduction form of ax-2 7. (Contributed by NM, 23-Jun-1994.)
Hypothesis
Ref Expression
a2d.1
Assertion
Ref Expression
a2d

Proof of Theorem a2d
StepHypRef Expression
1 a2d.1 . 2
2 ax-2 7 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  mpdd  40  imim2d  52  imim3i  59  loowoz  104  cbv1  2017  ralimdaaOLD  2860  ralimdva  2865  reuss2  3777  ssrel  5096  ssrel2  5098  ssrelrel  5108  funfvima2  6148  isofrlem  6236  dfwe2  6617  tfindsg  6695  tfinds2  6698  tfinds3  6699  ordom  6709  findsg  6727  finds2  6728  tfrlem1  7064  tfr3  7087  tz7.48lem  7125  oaordi  7214  oeordi  7255  nnaordi  7286  nnawordi  7289  nneneq  7720  ac6sfi  7784  domunfican  7813  fodomfi  7819  finsschain  7847  marypha1lem  7913  inf3lem2  8067  inf3lem5  8070  cantnfval2  8109  cantnflt  8112  cantnfp1lem3  8120  cantnfval2OLD  8139  cantnfltOLD  8142  cantnfp1lem3OLD  8146  cnfcom  8165  cnfcomOLD  8173  dfac12lem3  8546  ackbij1lem16  8636  sornom  8678  infpssrlem4  8707  fin23lem34  8747  fin23lem36  8749  isf32lem1  8754  isf32lem2  8755  zorn2lem4  8900  zorn2lem5  8901  zorn2lem6  8902  zorn2lem7  8903  ttukeylem5  8914  pwfseqlem3  9059  wunfi  9120  grudomon  9216  prlem934  9432  sup2  10524  nnaddcl  10583  nnmulcl  10584  peano5uzi  10976  uzind2  10980  uzindOLD  10982  nn0indd  10986  fzind  10987  zindd  10990  uzaddcl  11166  uzwo  11173  uzwoOLD  11174  om2uzlti  12061  seqcl2  12125  seqfveq2  12129  seqshft2  12133  monoord  12137  seqsplit  12140  seqcaopr3  12142  seqf1olem2a  12145  seqf1o  12148  seqid2  12153  seqhomo  12154  ser1const  12163  expcllem  12177  expeq0  12196  mulexp  12205  expadd  12208  expmul  12211  leexp2r  12223  leexp1a  12224  bernneq  12292  modexp  12301  facdiv  12365  facwordi  12367  faclbnd  12368  faclbnd4lem4  12374  faclbnd6  12377  hashgadd  12445  hashmap  12493  hashf1lem2  12505  hashf1  12506  seqcoll  12512  cshweqrep  12789  cjexp  12983  absexp  13137  rlimsqzlem  13471  lo1le  13474  iseraltlem2  13505  fsum2d  13586  modfsummod  13608  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  binom  13642  bcxmas  13647  climcndslem1  13661  climcndslem2  13662  cvgrat  13692  clim2prod  13697  prodfn0  13703  prodfrec  13704  ntrivcvgfvn0  13708  fprodabs  13778  fprod2d  13785  fprodefsum  13830  demoivreALT  13936  ruclem8  13970  ruclem9  13971  dvdsfac  14041  bitsinv1  14092  sadcadd  14108  sadadd2  14110  saddisjlem  14114  smuval2  14132  smupvallem  14133  smu01lem  14135  smupval  14138  smueqlem  14140  smumullem  14142  gcdmultiple  14188  rplpwr  14194  nn0seqcvgd  14199  seq1st  14200  alginv  14204  algcvga  14208  algfx  14209  prmdvdsexp  14255  prmfac1  14259  eulerthlem2  14312  pcmpt  14411  pcfac  14418  prmpwdvds  14422  prmreclem4  14437  vdwlem10  14508  ramcl  14547  mreexexd  15045  frmdgsum  16030  mulgnnass  16170  mhmmulg  16174  gsumwrev  16401  gsmsymgrfix  16453  gsmsymgreq  16457  sylow1lem1  16618  efginvrel2  16745  efgsrel  16752  gsum2dlem2  16998  gsum2dOLD  17000  ablfac1eulem  17123  pgpfac  17135  srgmulgass  17182  srgpcomp  17183  srgbinom  17196  lmodvsmmulgdi  17547  assamulgscm  17999  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  mptcoe1fsupp  18255  coe1fzgsumdlem  18343  coe1fzgsumd  18344  gsummoncoe1  18346  evl1gsumdlem  18392  evl1gsumd  18393  cnfldexp  18451  mdetunilem9  19122  mptcoe1matfsupp  19303  mp2pm2mplem4  19310  chpdmat  19342  tgcl  19471  fiuncmp  19904  2ndcsep  19960  1stcelcls  19962  ptcmpfi  20314  tmdmulg  20591  tmdgsum  20594  imasdsf1olem  20876  fsumcn  21374  caubl  21746  caublcls  21747  ovolunlem1a  21907  ovolfiniun  21912  ovolicc2lem3  21930  volfiniun  21957  voliunlem1  21960  volsuplem  21965  volsup  21966  dyadmax  22007  itgfsum  22233  dvnadd  22332  dvnres  22334  cpnord  22338  dvnfre  22355  dvmptfsum  22376  ply1divex  22537  fta1g  22568  plyco  22638  dgrcolem1  22670  dgrco  22672  dvnply2  22683  plydivex  22693  aaliou3lem2  22739  dvntaylp  22766  taylthlem1  22768  cxpmul2  23070  jensen  23318  ftalem2  23347  bcmono  23552  bposlem5  23563  lgsquad2lem2  23634  dchrisumlem1  23674  dchrisum0flb  23695  pntpbnd1  23771  pntlemf  23790  qabvle  23810  qabvexp  23811  ostthlem2  23813  ostth2lem2  23819  rusgranumwlk  24957  eupath2  24980  gxnn0add  25276  gxnn0mul  25279  ipasslem1  25746  mdslmd1lem1  27244  mdslmd1lem2  27245  iuninc  27428  ssrelf  27466  nn0min  27611  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  ofldchr  27804  cmppcmp  27861  nexple  28005  esumfzf  28075  sseqp1  28334  rrvsum  28393  signstfvc  28531  subfacp1lem6  28629  cvmliftlem7  28736  cvmliftlem10  28739  mrsubvrs  28882  iprodefisumlem  29123  binomfallfac  29163  faclimlem1  29168  trpredmintr  29314  wfr3g  29342  frr3g  29386  bpolycl  29814  onsuct0  29906  findfvcl  29917  sdclem2  30235  seqpo  30240  incsequz  30241  mettrifi  30250  heiborlem4  30310  bfplem1  30318  incssnn0  30643  mzpexpmpt  30677  pell14qrexpclnn0  30802  monotuz  30877  expmordi  30883  rmxypos  30885  jm2.17a  30898  jm2.17b  30899  rmygeid  30902  jm2.18  30930  jm2.19lem3  30933  jm2.15nn0  30945  jm2.16nn0  30946  dfac11  31008  pwslnm  31040  hbtlem5  31077  cnsrexpcl  31114  dvgrat  31193  lmodvsmdi  32975  bnj1174  34059  bj-imim2ALT  34167  bj-cbv1v  34292  pclfinclN  35674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator