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

Theorem a1d 25
Description: Deduction introducing an embedded antecedent. Deduction form of ax-1 6 and a1i 11. (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 17 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:  2a1d  26  a1i13  27  syl5com  31  mpid  42  syld  45  imim2d  54  syl6ci  68  syl5d  70  syl6d  72  pm2.21d  111  pm2.24d  141  pm2.51  160  pm2.521  161  pm2.61iii  174  mtod  184  impbid21d  196  imbi2d  325  adantr  474  jctild  558  jctird  559  pm3.4  576  anbi2d  727  anbi1d  728  ad4ant13  1274  ad4ant134  1278  ad4ant24  1280  meredith  1554  ax12  2224  nfsb4t  2272  ax12vALT  2311  moexex  2424  pm2.61da3ne  2766  ralrimivw  2845  reximdv  2892  rexlimdvw  2909  reuind  3267  sbcimdv  3353  rexn0  3899  eqoreldif  4041  tppreqb  4142  prnebg  4187  elpreqprlem  4190  axsep  4557  dtru  4633  otsndisj  4747  otiunsndisj  4748  fr0  4859  ssrel2  4972  poltletr  5282  ordsssuc2  5562  ndmfv  5952  fveqres  5964  fmptco  6124  tpres  6185  fntpb  6192  elunirn  6227  isof1oopb  6289  ndmovord  6534  ordsucelsuc  6726  tfinds  6763  tfindsg  6764  limomss  6774  findsg  6797  finds1  6799  xpexr  6810  bropopvvv  6953  bropfvvvvlem  6954  bropfvvvv  6955  soxp  6988  suppun  7013  extmptsuppeq  7017  funsssuppss  7019  suppss  7023  suppssov1  7025  suppss2  7027  suppssfv  7029  mpt2xopynvov0  7042  smofvon2  7152  oaordi  7324  oawordeulem  7332  odi  7357  brdomg  7662  map1  7732  fopwdom  7764  fodomr  7807  mapxpen  7822  infensuc  7834  onomeneq  7846  fineqvlem  7870  fineqv  7871  xpfi  7927  finsschain  7966  fsuppun  7987  fsuppunbi  7989  funsnfsupp  7992  dffi3  8030  fisup2g  8067  fisupcl  8068  fiinf2g  8099  wemapso2  8151  en3lplem2  8205  inf3lemd  8217  r1ordg  8334  r1val1  8342  r1pw  8401  r1pwALT  8402  rankxplim3  8437  carddomi2  8489  fidomtri  8512  pr2ne  8521  alephon  8585  alephcard  8586  alephnbtwn  8587  alephordi  8590  iunfictbso  8630  fin23lem30  8857  fin1a2lem10  8924  axdc3lem2  8966  axdc3lem4  8968  alephval2  9082  cfpwsdom  9094  axextnd  9101  axrepnd  9104  axpownd  9111  axregnd  9114  axinfndlem1  9115  fpwwe2lem12  9151  wunfi  9231  addnidpi  9411  pinq  9437  mulgt0sr  9614  dedekind  9882  nnind  10716  nn1m1nn  10718  nn0n0n1ge2b  11024  nn0lt2  11090  uzm1  11280  uzinfi  11329  nn01to3  11348  xrltnsym  11527  xrlttri  11529  xrlttr  11530  qbtwnxr  11586  xltnegi  11602  xlt2add  11641  xrsupsslem  11687  xrinfmsslem  11688  xrub  11692  reltxrnmnf  11727  fzospliti  12051  elfzonlteqm1  12092  elfznelfzo  12120  injresinjlem  12131  injresinj  12132  modfzo0difsn  12270  addmodlteq  12273  ssnn0fi  12311  fsuppmapnn0fiub0  12319  suppssfz  12320  seqfveq2  12349  seqshft2  12353  monoord  12357  seqsplit  12360  seqf1o  12368  seqhomo  12374  faclbnd4lem4  12595  hasheqf1oi  12649  hasheqf1oiOLD  12650  hashrabsn1  12671  hashgt0elex  12696  hash1snb  12714  hashf1lem2  12742  hashf1  12743  seqcoll  12750  pr2pwpr  12759  hashge2el2difr  12761  2swrd1eqwrdeq  12944  swrdswrd  12950  swrdccatin1  12972  swrdccatin12lem3  12979  swrdccat3  12981  swrdccat3blem  12984  repsdf2  13014  repswsymballbi  13016  cshw0  13029  cshwmodn  13030  cshwn  13032  cshwcl  13033  cshwlen  13034  cshw1  13057  2cshwcshw  13060  cshimadifsn  13064  s3sndisj  13192  s3iunsndisj  13193  relexprelg  13261  relexpnndm  13264  relexpaddg  13276  relexpaddd  13277  resqrex  13474  rexuz3  13571  rexanuz2  13572  limsupgre  13702  limsupgreOLD  13703  rlimconst  13768  caurcvg  13902  caurcvgOLD  13903  caucvg  13905  sumss  13950  fsumcl2lem  13957  modfsummods  14013  fsumrlim  14031  fsumo1  14032  fprodcl2lem  14164  nn0seqcvgd  14691  lcmdvds  14735  lcmfunsnlem2  14775  lcmfunsnlem  14776  exprmfct  14810  rpexp1i  14835  pcz  14992  pcadd  14996  pcmptcl  14998  prmgaplem5  15187  prmgaplem6  15188  prmgaplem7  15189  cshwshashlem1  15227  cshwsdisj  15230  prmlem0  15238  ressress  15352  initoeu2lem2  16076  mgm2nsgrplem2  16813  mgm2nsgrplem3  16814  symgextf1  17223  gsmsymgrfix  17230  gsmsymgreq  17234  sylow1lem1  17411  efgsf  17540  efgrelexlema  17560  dprdss  17822  ablfac1eulem  17865  lssssr  18336  01eq0ring  18655  psrvscafval  18773  mplcoe1  18848  mplcoe5  18851  mpfrcl  18900  psgnodpm  19314  mamudm  19571  matmulcell  19628  dmatmul  19680  scmatsgrp1  19705  mavmuldm  19733  mavmulsolcl  19734  mdetunilem9  19803  cramerlem3  19872  cramer0  19873  chpscmatgsumbin  20026  chp0mat  20028  fvmptnn04ifc  20034  fvmptnn04ifd  20035  epttop  20181  neiptopnei  20305  fiuncmp  20576  1stcrest  20625  comppfsc  20704  kgenss  20715  hmeofval  20930  fbun  21013  fgss2  21047  filuni  21058  filssufilg  21084  filufint  21093  hausflimi  21153  hausflim  21154  hauspwpwf1  21160  fclscmp  21203  alexsubALTlem4  21223  ptcmplem3  21227  ptcmplem5  21229  cstucnd  21457  isxmet2d  21500  imasdsf1olem  21546  blfps  21579  blf  21580  metrest  21697  nrginvrcn  21852  nmoge0  21884  nmoleub  21894  nmoge0OLD  21902  nmoleubOLD  21910  fsumcn  22060  cmetcaulem  22417  iscmet3  22422  iscmet2  22423  bcthlem2  22452  ovolicc2lem3  22631  itg2seq  22861  itg2splitlem  22867  itgeq1f  22890  itgeq2  22896  iblcnlem  22907  itgfsum  22945  limcnlp  22994  perfdvf  23019  dvnres  23046  dvmptfsum  23088  c1lip1  23110  abelth  23557  sinq12ge0  23624  rlimcnp  24052  xrlimcnp  24055  jensen  24075  ppiublem1  24291  dchrelbas3  24327  bcmono  24366  lgsquad2lem2  24448  2sqlem10  24463  pntrsumbnd2  24566  pntpbnd1  24585  pntlem3  24608  axcontlem7  25161  ausisusgra  25243  usgraidx2v  25281  nbgra0nb  25318  nbgranself2  25325  nbgraf1olem3  25332  nbgraf1olem5  25334  nb3graprlem1  25340  nbcusgra  25352  cusgrasizeinds  25365  usgra2wlkspthlem1  25508  wwlkm1edg  25624  wwlknfi  25627  clwwlkprop  25659  clwwlknprop  25661  clwlkisclwwlklem2a  25674  el2wlkonotot0  25760  usg2wlkonot  25771  usg2wotspth  25772  2spontn0vne  25775  vdgrf  25786  cusgraiffrusgra  25828  rusgraprop4  25832  rusgrasn  25833  eupai  25855  eupath2  25868  frgra2v  25887  frgra3vlem1  25888  3vfriswmgralem  25892  1to2vfriswmgra  25894  1to3vfriswmgra  25895  2pthfrgra  25899  vdfrgra0  25910  vdgn1frgrav2  25914  frgrawopreglem2  25933  frgrawopreglem3  25934  frgrawopreglem4  25935  frgrawopreg  25937  frgraregorufr0  25940  frgraregorufr  25941  2spotdisj  25949  2spotiundisj  25950  2spotmdisj  25956  numclwwlkovf2ex  25974  extwwlkfab  25978  frgrareggt1  26004  frgrareg  26005  frgraregord13  26007  aevdemo  26059  isexid2  26216  zerdivemp1  26325  shsvs  27139  0cnop  27795  0cnfn  27796  cnlnssadj  27896  ssmd1  28127  ssmd2  28128  atexch  28197  mdsymlem4  28222  sumdmdlem  28234  ifeqeqx  28318  fmptcof2  28416  padct  28463  nnindf  28538  pwsiga  29107  ldsysgenld  29137  fiunelros  29151  bnj151  29840  bnj594  29875  bnj600  29882  subfacp1lem6  30060  erdszelem8  30073  cvmliftlem7  30166  cvmliftlem10  30169  cvmlift2lem12  30189  mrsubfval  30298  msubfval  30314  mclsssvlem  30352  trpredlem1  30619  poseq  30642  funpartfv  30863  endofsegid  31003  broutsideof2  31040  a1i24  31106  nn0prpwlem  31127  nn0prpw  31128  ordcmp  31256  findreccl  31262  bj-alsb  31420  bj-ax6e  31448  bj-ax12v  31561  bj-axsep  31590  bj-dtru  31594  bj-xpnzex  31738  bj-xnex  31844  finxp00  32015  wl-spae  32083  wl-nfs1t  32102  poimirlem27  32205  ovoliunnfl  32220  voliunnfl  32222  volsupnfl  32223  itg2addnclem3  32233  itg2addnc  32234  ftc1anc  32263  areacirclem1  32270  sdclem2  32308  fdc  32311  mettrifi  32323  zerdivemp1x  32431  smprngopr  32522  mpt2bi123f  32642  mptbi12f  32646  ac6s6  32651  jca3  32658  ax12o  32708  hbequid  32713  dvelimf-o  32733  ax12eq  32745  ax12el  32746  ax12indalem  32749  ax12inda2ALT  32750  ax12inda2  32751  lfl1dim  32927  lfl1dim2N  32928  lkreqN  32976  cvrexchlem  33224  ps-2  33283  paddasslem14  33638  idldil  33919  isltrn2N  33925  cdleme25a  34160  dibglbN  34974  dihlsscpre  35042  dvh4dimlem  35251  lcfl7N  35309  mapdval2N  35438  monotoddzzfi  36030  rp-fakeimass  36396  clublem  36456  relexpnul  36509  ee121  37217  ee122  37218  rspsbc2  37251  ax6e2ndeq  37282  vd12  37332  vd13  37333  ee221  37382  ee212  37384  ee112  37387  ee211  37390  ee210  37392  ee201  37394  ee120  37396  ee021  37398  ee012  37400  ee102  37402  ee03  37476  ee31  37487  ee31an  37489  ee123  37498  ax6e2ndeqVD  37654  ax6e2ndeqALT  37676  refsum2cnlem1  37706  fiiuncl  37748  disjrnmpt2  37823  disjinfi  37828  mccl  38080  constlimc  38108  limclner  38136  ioodvbdlimc1lem2  38223  ioodvbdlimc1lem2OLD  38225  ioodvbdlimc2lem  38227  ioodvbdlimc2lemOLD  38228  dvmptfprod  38239  dvnprodlem3  38242  stoweidlem31  38328  pwsal  38620  prsal  38623  sge0pnffigt  38684  sge0ltfirp  38688  0ome  38814  hoicvrrex  38841  hoidmvle  38885  ovnhoilem1  38886  ovnlecvr2  38895  reuan  39121  2reu4  39131  funressnfv  39149  ndmaovass  39228  nltle2tri  39236  smonoord  39238  mod2eq1n2dvds  39245  iccpartigtl  39257  icceuelpartlem  39269  iccpartnel  39272  nn0o1gt2ALTV  39343  nn0oALTV  39345  stgoldbwt  39397  bgoldbwt  39398  sgoldbalt  39402  nnsum3primesgbe  39407  wtgoldbnnsum4prm  39417  bgoldbnnsum3prm  39419  bgoldbtbndlem2  39421  bgoldbtbndlem3  39422  bgoldbtbndlem4  39423  bgoldbtbnd  39424  bgoldbachlt  39426  tgblthelfgott  39428  pfxccat3  39489  n0snor2el  39518  propeqop  39521  propssopi  39522  ssprsseq  39524  otiunsndisjX  39527  funsndifnop  39543  fundmge2nop0  39547  fzoopth  39585  xnn0xaddcl  39613  ausgrusgrb  39795  usgredg2v  39854  lfuhgr1v0e  39880  subumgredg2  39909  fusgrfisbase  39947  nbuhgr  39965  uhgrnbgr0nb  39976  nbgr0vtxlem  39977  nbgr1vtx  39980  uvtxa0  40020  uvtx2vtx1edg  40025  cusgredg  40046  cusgrsizeinds  40068  sizusglecusg  40079  ewlkle  40207  upgr1wlkwlk  40247  pthdivtx  40335  usgr2trlncl  40366  cyclnsPth  40406  crctcsh1wlkn0lem4  40416  wwlksn  40440  iswwlksnon  40451  iswspthsnon  40452  wwlksm1edg  40478  wwlksnfi  40512  wwlksnonfi  40527  wspn0  40531  2pthdlem1  40537  umgr2wlk  40556  2wspdisj  40565  2wspiundisj  40566  clwwlksn  40589  clwlkclwwlklem2a  40607  clwlkclwwlk  40611  umgrclwwlksge2  40619  clwwlksnfi  40620  clwwisshclwws  40635  clwwnisshclwwsn  40637  3pthdlem1  40731  eupth2  40807  nfrgr2v  40842  frgr3vlem1  40843  1to2vfriswmgr  40849  1to3vfriswmgr  40850  vdgn1frgrv2  40866  frgrwopreglem3  40883  frgrwopreglem4  40884  frgrwopreg  40886  frgrregorufr0  40889  frgrregorufr  40890  fusgr2wsp2nb  40898  2wspmdisj  40901  av-numclwwlkovf2ex  40917  av-extwwlkfab  40920  av-frgrareggt1  40947  av-frgrareg  40948  av-frgraregord13  40950  nrhmzr  41063  rngccatidALTV  41181  funcrngcsetcALT  41191  ringccatidALTV  41244  nn0le2is012  41338  lincdifsn  41407  lindslinindimp2lem1  41441  lindsrng01  41451  ldepsnlinc  41491  m1modmmod  41513  nno  41517  blen1b  41588  nn0sumshdiglemB  41620  nn0sumshdiglem1  41621
  Copyright terms: Public domain W3C validator