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

Theorem a1d 25
Description: Deduction introducing an embedded antecedent. Deduction form of ax-1 6. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Hypothesis
Ref Expression
a1d.1
Assertion
Ref Expression
a1d

Proof of Theorem a1d
StepHypRef Expression
1 a1d.1 . 2
2 ax-1 6 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  a1iiOLD  28  syl5com  30  mpid  41  syld  44  imim2d  52  syl6ci  65  syl5d  67  syl6d  69  pm2.21d  106  pm2.24d  143  pm2.51  153  pm2.521  154  pm2.61iii  167  mtod  177  impbid21d  190  imbi2d  316  adantr  465  jctild  543  jctird  544  pm3.4  561  anbi2d  703  anbi1d  704  3ecase  1333  meredith  1472  nfsb4t  2130  ax12vALT  2171  ax12  2234  hbequid  2239  dvelimf-o  2259  ax12eq  2271  ax12el  2272  ax12indalem  2275  ax12inda2ALT  2276  ax12inda2  2277  morimOLD  2341  moexex  2363  pm2.61da3ne  2777  ralrimivw  2872  rgen2aOLD  2885  reximdv  2931  rexlimdvw  2952  reuind  3303  sbcimdv  3396  rexn0  3932  tppreqb  4171  prnebg  4212  axsep  4572  dtru  4643  reusv6OLD  4663  reusv7OLD  4664  otsndisj  4757  otiunsndisj  4758  fr0  4863  ordsssuc2  4971  ssrel2  5098  poltletr  5407  ndmfv  5895  fveqres  5905  fmptco  6064  elunirn  6163  ndmovord  6465  ordsucelsuc  6657  tfinds  6694  tfindsg  6695  limomss  6705  findsg  6727  finds1  6729  xpexr  6740  bropopvvv  6880  soxp  6913  suppun  6939  extmptsuppeq  6943  funsssuppss  6945  suppss  6949  suppssov1  6951  suppss2  6953  suppssfv  6955  supp0cosupp0  6958  imacosupp  6959  mpt2xopynvov0  6965  smofvon2  7046  oaordi  7214  oawordeulem  7222  odi  7247  brdomg  7546  map1  7614  fopwdom  7645  fodomr  7688  mapxpen  7703  infensuc  7715  onomeneq  7727  fineqvlem  7754  fineqv  7755  pssnn  7758  xpfi  7811  finsschain  7847  suppeqfsuppbi  7863  fsuppun  7868  fsuppunbi  7870  funsnfsupp  7873  dffi3  7911  fisup2g  7947  fisupcl  7948  wemapso2  8000  en3lplem2  8053  inf3lemd  8065  r1ordg  8217  r1val1  8225  r1pw  8284  r1pwOLD  8285  rankxplim3  8320  carddomi2  8372  fidomtri  8395  pr2ne  8404  alephon  8471  alephcard  8472  alephnbtwn  8473  alephordi  8476  iunfictbso  8516  fin23lem30  8743  fin1a2lem10  8810  domtriomlem  8843  axdc3lem2  8852  axdc3lem4  8854  alephval2  8968  cfpwsdom  8980  axextnd  8987  axrepnd  8990  axpownd  8999  axregnd  9002  axregndOLD  9003  axinfndlem1  9004  fpwwe2lem12  9040  wunfi  9120  addnidpi  9300  pinq  9326  ltexprlem7  9441  mulgt0sr  9503  dedekind  9765  nnind  10579  nn1m1nn  10581  nn0n0n1ge2b  10885  nn0lt2  10952  uzindOLD  10982  uzm1  11140  nn01to3  11204  xrltnsym  11372  xrlttri  11374  xrlttr  11375  qbtwnxr  11428  xltnegi  11444  xlt2add  11481  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  fzospliti  11857  elfzonlteqm1  11891  elfznelfzo  11915  injresinjlem  11925  injresinj  11926  ssnn0fi  12094  fsuppmapnn0fiubex  12098  fsuppmapnn0fiub0  12099  suppssfz  12100  seqfveq2  12129  seqshft2  12133  monoord  12137  seqsplit  12140  seqf1o  12148  seqhomo  12154  faclbnd4lem4  12374  hasheqf1oi  12424  hashrabsn1  12442  hashgt0elex  12466  hash1snb  12479  hashf1lem2  12505  hashf1  12506  seqcoll  12512  hash2prd  12518  pr2pwpr  12520  ccatval1lsw  12602  swrdnd  12657  swrdvalodm2  12664  2swrd1eqwrdeq  12679  swrdswrd  12685  swrdccatin1  12708  swrdccatin12lem3  12715  swrdccat3  12717  swrdccat3blem  12720  repsdf2  12750  repswsymballbi  12752  cshw0  12765  cshwmodn  12766  cshwn  12768  cshwcl  12769  cshwlen  12770  cshw1  12790  2cshwcshw  12793  resqrex  13084  rexuz3  13181  rexanuz2  13182  limsupgre  13304  rlimconst  13367  caurcvg  13499  caucvg  13501  sumss  13546  fsumcl2lem  13553  modfsummods  13607  fsumrlim  13625  fsumo1  13626  fprodcl2lem  13757  nn0seqcvgd  14199  exprmfct  14251  rpexp1i  14262  pcz  14404  pcadd  14408  pcmptcl  14410  cshwsidrepswmod0  14579  cshwshashlem1  14580  cshwshashlem2  14581  cshwsdisj  14583  prmlem0  14591  ressress  14694  mgm2nsgrplem2  16037  mgm2nsgrplem3  16038  symgextf1  16446  gsmsymgrfix  16453  gsmsymgreq  16457  psgnunilem4  16522  sylow1lem1  16618  efgsf  16747  efgrelexlema  16767  dprdss  17076  ablfac1eulem  17123  lssssr  17599  01eq0ring  17920  psrvscafval  18043  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  mpfrcl  18187  psgnodpm  18624  mamudm  18890  mamufacex  18891  matmulcell  18947  dmatmul  18999  scmatsgrp1  19024  mavmuldm  19052  mavmulsolcl  19053  mdetunilem9  19122  cramerlem3  19191  cramer0  19192  chpscmatgsumbin  19345  chp0mat  19347  fvmptnn04ifc  19353  fvmptnn04ifd  19354  epttop  19510  neiptopnei  19633  cmpsublem  19899  fiuncmp  19904  1stcrest  19954  comppfsc  20033  kgenss  20044  hmeofval  20259  fbun  20341  fgss2  20375  filcon  20384  filuni  20386  filssufilg  20412  filufint  20421  hausflimi  20481  hausflim  20482  hauspwpwf1  20488  fclscmp  20531  alexsubALTlem4  20550  ptcmplem3  20554  ptcmplem5  20556  cstucnd  20787  isxmet2d  20830  imasdsf1olem  20876  blfps  20909  blf  20910  metrest  21027  nrginvrcn  21200  nmoge0  21228  nmoleub  21238  fsumcn  21374  cmetcaulem  21727  iscmet3  21732  iscmet2  21733  bcthlem2  21764  ovolicc2lem3  21930  itg2seq  22149  itg2splitlem  22155  itgeq1f  22178  itgeq2  22184  iblcnlem  22195  itgfsum  22233  limcnlp  22282  perfdvf  22307  dvnres  22334  dvmptfsum  22376  c1lip1  22398  aalioulem5  22732  abelth  22836  sinq12ge0  22901  rlimcnp  23295  xrlimcnp  23298  jensen  23318  ppiublem1  23477  dchrelbas3  23513  bcmono  23552  lgsquad2lem2  23634  2sqlem10  23649  pntrsumbnd2  23752  pntpbnd1  23771  pntlem3  23794  axlowdimlem15  24259  axcontlem7  24273  ausisusgra  24355  usgraidx2v  24393  nbgra0nb  24429  nbgranself2  24436  nbgraf1olem3  24443  nbgraf1olem5  24445  nb3graprlem1  24451  nbcusgra  24463  cusgrasizeinds  24476  uvtxnbgra  24493  wlkdvspthlem  24609  usgra2wlkspthlem1  24619  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  wwlkm1edg  24735  wwlknfi  24738  clwwlkprop  24770  clwwlkgt0  24771  clwwlknprop  24772  clwlkisclwwlklem2a  24785  el2wlkonotot0  24872  usg2wlkonot  24883  usg2wotspth  24884  2spontn0vne  24887  vdgrf  24898  nbhashuvtx1  24915  cusgraiffrusgra  24940  rusgraprop4  24944  rusgrasn  24945  eupai  24967  eupath2  24980  frgra2v  24999  frgra3vlem1  25000  3vfriswmgralem  25004  1to2vfriswmgra  25006  1to3vfriswmgra  25007  2pthfrgra  25011  frgranbnb  25020  vdfrgra0  25022  vdn1frgrav2  25025  vdgn1frgrav2  25026  vdgfrgragt2  25027  frgrawopreglem2  25045  frgrawopreglem3  25046  frgrawopreglem4  25047  frgrawopreg  25049  frgraregorufr0  25052  frgraregorufr  25053  2spotdisj  25061  2spotiundisj  25062  2spotmdisj  25068  numclwwlkovf2ex  25086  extwwlkfab  25090  frgrareggt1  25116  frgrareg  25117  frgraregord13  25119  isexid2  25327  zerdivemp1  25436  shsvs  26241  0cnop  26898  0cnfn  26899  cnlnssadj  26999  ssmd1  27230  ssmd2  27231  atexch  27300  mdsymlem4  27325  sumdmdlem  27337  ifeqeqx  27419  fmptcof2  27502  nnindf  27610  pwsiga  28130  subfacp1lem6  28629  erdszelem8  28642  cvmliftlem7  28736  cvmliftlem10  28739  cvmlift2lem12  28759  mrsubfval  28868  msubfval  28884  mclsssvlem  28922  trpredlem1  29310  poseq  29333  funpartfv  29595  endofsegid  29735  broutsideof2  29772  ordcmp  29912  findreccl  29918  wl-nfs1t  29991  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  itg2addnclem3  30068  itg2addnc  30069  ftc1anc  30098  areacirclem1  30107  a1i13  30113  a1i24  30116  nn0prpwlem  30140  nn0prpw  30141  sdclem2  30235  fdc  30238  mettrifi  30250  zerdivemp1x  30358  smprngopr  30449  mpt2bi123f  30571  mptbi12f  30575  ac6s6  30580  jca3  30587  monotoddzzfi  30878  lcmdvds  31214  refsum2cnlem1  31412  mccl  31606  constlimc  31630  limclner  31657  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvmptfprod  31742  dvnprodlem3  31745  stoweidlem31  31813  reuan  32185  2reu4  32195  funressnfv  32213  ndmaovass  32291  otiunsndisjX  32301  fzoopth  32340  usgra2pthspth  32351  usgra2pth  32354  usgedgvadf1  32415  usgedgvadf1ALT  32418  usgfis  32446  usgfisALT  32450  tpres  32554  initoeu2lem2  32621  nrhmzr  32679  rngccatidOLD  32797  funcrngcsetcALT  32807  ringccatidOLD  32860  nn0le2is012  32956  suppmptcfin  32972  lincdifsn  33025  linc1  33026  lindslinindimp2lem1  33059  lindslinindsimp2lem5  33063  lindsrng01  33069  ldepsnlinc  33109  ad4ant14  33225  ad4ant134  33228  ee121  33274  ee122  33275  rspsbc2  33305  ax6e2ndeq  33332  vd12  33386  vd13  33387  ee221  33436  ee212  33438  ee112  33441  ee211  33444  ee210  33446  ee201  33448  ee120  33450  ee021  33452  ee012  33454  ee102  33456  ee03  33538  ee31  33549  ee31an  33551  ee123  33560  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  bnj151  33935  bnj594  33970  bnj600  33977  bj-ax12v  34348  bj-axsep  34379  bj-dtru  34383  bj-xpnzex  34516  lfl1dim  34846  lfl1dim2N  34847  lkreqN  34895  cvrexchlem  35143  ps-2  35202  paddasslem14  35557  idldil  35838  isltrn2N  35844  cdleme25a  36079  dibglbN  36893  dihlsscpre  36961  dvh4dimlem  37170  lcfl7N  37228  mapdval2N  37357  rp-fakeimass  37736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator