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  44  syld  47  imim2d  57  syl6ci  71  syl5d  73  syl6d  75  pm2.21d  119  pm2.24d  148  pm2.51  166  pm2.521  167  pm2.61iii  179  mtod  189  impbid21d  201  imbi2d  329  adantr  466  jctild  511  jctird  512  anbi2d  608  anbi1d  609  pm3.4  804  ad4ant134OLD  1182  ad4ant13OLD  1207  meredith  1714  ax12  2460  nfsb4t  2536  ax12vALT  2575  moexex  2690  pm2.61da3ne  3032  ralrimivw  3116  reximdv  3164  rexlimdvw  3182  reuind  3564  rexn0  4216  tppreqb  4472  ssprsseq  4492  n0snor2el  4498  prnebg  4521  prel12g  4531  elpreqprlem  4533  3elpr2eq  4574  disjord  4776  disjiund  4778  axsep  4915  dtru  4989  propssopi  5102  opthhausdorff  5111  fr0  5229  ssrel2  5351  poltletr  5670  ordsssuc2  5958  ordnbtwn  5960  ndmfv  6360  fveqres  6372  fmptco  6540  funsndifnop  6560  tpres  6611  fntpb  6618  elunirn  6653  isof1oopb  6719  fvmptopab  6845  ndmovord  6972  ordsucelsuc  7170  tfinds  7207  tfindsg  7208  limomss  7218  findsg  7241  finds1  7243  xpexr  7254  bropopvvv  7407  bropfvvvvlem  7408  bropfvvvv  7409  soxp  7442  suppun  7467  extmptsuppeq  7471  funsssuppss  7474  suppss  7478  suppssov1  7480  suppss2  7482  suppssfv  7484  mpt2xopynvov0  7497  smofvon2  7607  oaordi  7781  oawordeulem  7789  odi  7814  brdomg  8120  snmapen  8191  fopwdom  8225  fodomr  8268  mapxpen  8283  infensuc  8295  onomeneq  8307  fineqvlem  8331  fineqv  8332  xpfi  8388  finsschain  8430  fsuppun  8451  fsuppunbi  8453  funsnfsupp  8456  dffi3  8494  fisup2g  8531  fisupcl  8532  fiinf2g  8563  wemapso2  8615  epnsym  8669  en3lplem2  8673  preleqg  8675  inf3lemd  8689  r1ordg  8806  r1val1  8814  r1pw  8873  r1pwALT  8874  rankxplim3  8909  eldju2ndl  8951  eldju2ndr  8952  carddomi2  8997  fidomtri  9020  pr2ne  9029  alephon  9093  alephcard  9094  alephnbtwn  9095  alephordi  9098  iunfictbso  9138  fin23lem30  9367  fin1a2lem10  9434  axdc3lem2  9476  axdc3lem4  9478  alephval2  9597  cfpwsdom  9609  axextnd  9616  axrepnd  9619  axpownd  9626  axregnd  9629  axinfndlem1  9630  fpwwe2lem12  9666  wunfi  9746  addnidpi  9926  pinq  9952  mulgt0sr  10129  dedekind  10403  nnind  11241  nn1m1nn  11243  nn0n0n1ge2b  11562  nn0lt2  11643  nn0le2is012  11644  uzm1  11921  uzinfi  11972  nn01to3  11985  xrltnsym  12176  xrlttri  12178  xrlttr  12179  qbtwnxr  12237  xltnegi  12253  xnn0xaddcl  12272  xlt2add  12296  xrsupsslem  12343  xrinfmsslem  12344  xrub  12348  reltxrnmnf  12378  fzospliti  12709  elfzonlteqm1  12753  elfznelfzo  12782  injresinjlem  12797  injresinj  12798  modfzo0difsn  12951  addmodlteq  12954  ssnn0fi  12993  fsuppmapnn0fiub0  13001  suppssfz  13002  seqfveq2  13031  monoord  13039  seqf1o  13050  seqhomo  13056  faclbnd4lem4  13288  hasheqf1oi  13345  hashrabsn1  13366  hashgt0elex  13392  hash1snb  13410  hashf1lem2  13443  hashf1  13444  seqcoll  13451  hashle2pr  13462  pr2pwpr  13464  hashge2el2difr  13466  2swrd1eqwrdeq  13664  swrdswrd  13670  swrdccatin1  13693  swrdccatin12lem3  13700  swrdccat3  13702  swrdccat3blem  13705  repsdf2  13735  repswsymballbi  13737  cshw0  13750  cshwmodn  13751  cshwn  13753  cshwcl  13754  cshwlen  13755  cshw1  13778  2cshwcshw  13781  cshimadifsn  13785  s3sndisj  13917  s3iunsndisj  13918  relexprelg  13987  relexpnndm  13990  relexpaddg  14002  relexpaddd  14003  resqrex  14200  rexuz3  14297  rexanuz2  14298  limsupgre  14421  rlimconst  14484  caurcvg  14616  caucvg  14618  sumss  14664  fsumcl2lem  14671  modfsummods  14733  fsumrlim  14751  fsumo1  14752  fprodcl2lem  14888  dvdsaddre2b  15239  dvdsabseq  15245  mod2eq1n2dvds  15280  nno  15307  sumeven  15319  sumodd  15320  nn0seqcvgd  15492  lcmdvds  15530  lcmfunsnlem2  15562  lcmfunsnlem  15563  divgcdcoprm0  15587  exprmfct  15624  rpexp1i  15641  prm23lt5  15727  prm23ge5  15728  pcz  15793  pcadd  15801  pcmptcl  15803  oddprmdvds  15815  prmgaplem5  15967  prmgaplem6  15968  prmgaplem7  15969  cshwshashlem1  16010  cshwsdisj  16013  prmlem0  16020  setsstruct  16106  ressress  16147  initoeu2lem2  16873  mgm2nsgrplem2  17615  mgm2nsgrplem3  17616  dfgrp2e  17657  dfgrp3e  17724  symgextf1  18049  gsmsymgrfix  18056  gsmsymgreq  18060  sylow1lem1  18221  efgsf  18350  efgrelexlema  18370  dprdss  18637  ablfac1eulem  18680  lssssr  19166  lssssrOLD  19167  01eq0ring  19488  psrvscafval  19606  mplcoe1  19681  mplcoe5  19684  mpfrcl  19734  psgnodpm  20150  mamudm  20412  matmulcell  20469  matmulcellOLD  20470  dmatmul  20522  scmatsgrp1  20547  mavmuldm  20575  mavmulsolcl  20576  mdetunilem9  20645  cramerlem3  20716  cramer0  20717  chpscmatgsumbin  20870  chp0mat  20872  fvmptnn04ifc  20878  fvmptnn04ifd  20879  epttop  21035  neiptopnei  21158  fiuncmp  21429  1stcrest  21478  comppfsc  21557  kgenss  21568  hmeofval  21783  fbun  21865  fgss2  21899  filuni  21910  filssufilg  21936  filufint  21945  hausflimi  22005  hausflim  22006  hauspwpwf1  22012  fclscmp  22055  alexsubALTlem4  22075  ptcmplem3  22079  ptcmplem5  22081  cstucnd  22309  isxmet2d  22353  imasdsf1olem  22399  blfps  22432  blf  22433  metrest  22550  nrginvrcn  22717  nmoge0  22746  nmoleub  22756  fsumcn  22894  cmetcaulem  23306  iscmet3  23311  iscmet2  23312  bcthlem2  23342  ovolicc2lem3  23508  itg2seq  23730  itg2splitlem  23736  itgeq1f  23759  itgeq2  23765  iblcnlem  23776  itgfsum  23814  limcnlp  23863  perfdvf  23888  dvnres  23915  dvmptfsum  23959  c1lip1  23981  abelth  24416  sinq12ge0  24482  rlimcnp  24914  xrlimcnp  24917  jensen  24937  ppiublem1  25149  dchrelbas3  25185  bcmono  25224  zabsle1  25243  gausslemma2dlem0f  25308  gausslemma2dlem1a  25312  gausslemma2dlem4  25316  lgsquad2lem2  25332  2lgslem1a1  25336  2lgslem3  25351  2lgs  25354  2lgsoddprm  25363  2sqlem10  25375  pntrsumbnd2  25478  pntpbnd1  25497  pntlem3  25520  axcontlem7  26072  ausgrusgrb  26283  usgredg2v  26342  lfuhgr1v0e  26370  subumgredg2  26401  upgrreslem  26420  umgrreslem  26421  fusgrfisbase  26444  nbuhgr  26463  uhgrnbgr0nb  26474  nbgr0vtxlem  26475  nbgr1vtx  26478  cusgredg  26556  cusgrsizeinds  26584  sizusglecusg  26595  finsumvtxdg2size  26682  ewlkle  26737  upgriswlk  26773  pthdivtx  26861  usgr2trlncl  26892  crctcshwlkn0lem4  26942  wwlksn  26966  iswwlksnon  26983  iswwlksnonOLD  26984  iswspthsnon  26987  iswspthsnonOLD  26988  wwlksm1edg  27016  wwlksnfi  27051  2pthdlem1  27078  umgr2wlk  27097  umgrclwwlkge2  27142  clwlkclwwlklem2a  27149  clwlkclwwlk  27153  clwlkclwwlkf1lem2  27156  clwlkclwwlkf  27159  clwwisshclwws  27166  clwwlknOLD  27180  clwwlknlbonbgr1  27196  clwwlknfi  27202  wwlksext2clwwlk  27215  clwwlknon0  27268  clwwlknonel  27270  clwwlknonwwlknonbOLD  27283  clwwlknonex2e  27287  3pthdlem1  27345  eupth2  27420  nfrgr2v  27455  frgr3vlem1  27456  1to2vfriswmgr  27462  1to3vfriswmgr  27463  vdgn1frgrv2  27479  frgrncvvdeqlem9  27490  frgrwopreglem4a  27493  frgrregorufr0  27507  frgrregorufr  27508  2wspmdisj  27520  2clwwlk2clwwlklem  27531  frgrreggt1  27593  frgrreg  27594  frgrregord13  27596  aevdemo  27660  shsvs  28523  0cnop  29179  0cnfn  29180  cnlnssadj  29280  ssmd1  29511  ssmd2  29512  atexch  29581  mdsymlem4  29606  sumdmdlem  29618  rabeqsnd  29681  ifeqeqx  29700  fmptcof2  29798  padct  29838  nnindf  29906  pwsiga  30534  ldsysgenld  30564  fiunelros  30578  breprexp  31052  bnj151  31286  bnj594  31321  bnj600  31328  subfacp1lem6  31506  erdszelem8  31519  cvmliftlem7  31612  cvmliftlem10  31615  cvmlift2lem12  31635  mrsubfval  31744  msubfval  31760  mclsssvlem  31798  trpredlem1  32064  poseq  32091  nolesgn2o  32162  funpartfv  32390  endofsegid  32530  broutsideof2  32567  a1i24  32633  nn0prpwlem  32655  nn0prpw  32656  ordcmp  32784  findreccl  32790  bj-alsb  32964  bj-ax6e  32991  bj-ax12v3ALT  33014  bj-axsep  33130  bj-dtru  33134  bj-xpnzex  33278  finxp00  33577  cnfinltrel  33579  wl-spae  33644  wl-nfs1t  33660  poimirlem27  33770  ovoliunnfl  33785  voliunnfl  33787  volsupnfl  33788  itg2addnclem3  33796  itg2addnc  33797  ftc1anc  33826  areacirclem1  33833  sdclem2  33871  fdc  33874  mettrifi  33886  isexid2  33987  zerdivemp1x  34079  smprngopr  34184  mpt2bi123f  34304  mptbi12f  34308  ac6s6  34313  relcnveq3  34436  elrelscnveq3  34584  jca3  34664  ax12fromc15  34714  hbequid  34718  dvelimf-o  34738  ax12eq  34750  ax12el  34751  ax12indalem  34754  ax12inda2ALT  34755  ax12inda2  34756  lfl1dim  34931  lfl1dim2N  34932  lkreqN  34980  cvrexchlem  35228  ps-2  35287  paddasslem14  35642  idldil  35923  isltrn2N  35929  cdleme25a  36163  dibglbN  36977  dihlsscpre  37045  dvh4dimlem  37254  lcfl7N  37312  mapdval2N  37441  monotoddzzfi  38034  rp-fakeimass  38384  clublem  38444  relexpnul  38497  ee121  39237  ee122  39238  rspsbc2  39270  ax6e2ndeq  39301  vd12  39351  vd13  39352  ee221  39401  ee212  39403  ee112  39406  ee211  39409  ee210  39411  ee201  39413  ee120  39415  ee021  39417  ee012  39419  ee102  39421  ee03  39494  ee31  39505  ee31an  39507  ee123  39516  ax6e2ndeqVD  39668  ax6e2ndeqALT  39690  refsum2cnlem1  39719  fiiuncl  39756  eliin2f  39809  disjrnmpt2  39896  disjinfi  39901  rnmptbd2lem  39982  rnmptbdlem  39989  allbutfi  40133  infxrunb3rnmpt  40172  infrpgernmpt  40212  monoordxrv  40229  mccl  40349  constlimc  40375  limclner  40402  xlimmnfvlem1  40577  xlimpnfvlem1  40581  ioodvbdlimc1lem2  40666  ioodvbdlimc2lem  40668  dvmptfprod  40679  dvnprodlem3  40682  stoweidlem31  40766  pwsal  41053  prsal  41056  sge0pnffigt  41131  sge0ltfirp  41135  0ome  41264  hoicvrrex  41291  hoidmvle  41335  ovnhoilem1  41336  ovnlecvr2  41345  smflimlem3  41502  reuan  41701  2reu4  41711  funressnfv  41729  ndmaovass  41807  otiunsndisjX  41822  nltle2tri  41852  fzoopth  41866  smonoord  41870  iccpartigtl  41888  icceuelpartlem  41900  iccpartnel  41903  pfxccat3  41955  fmtnoprmfac1  42006  fmtnoprmfac2  42008  prmdvdsfmtnof1lem2  42026  31prm  42041  lighneallem3  42053  lighneallem4b  42055  lighneallem4  42056  lighneal  42057  nn0o1gt2ALTV  42134  nn0oALTV  42136  odd2prm2  42156  even3prm2  42157  stgoldbwt  42193  sbgoldbwt  42194  sbgoldbalt  42198  sbgoldbo  42204  nnsum3primesgbe  42209  wtgoldbnnsum4prm  42219  bgoldbnnsum3prm  42221  bgoldbtbndlem2  42223  bgoldbtbndlem3  42224  bgoldbtbndlem4  42225  bgoldbtbnd  42226  bgoldbachlt  42230  tgblthelfgott  42232  bgoldbachltOLD  42236  tgblthelfgottOLD  42238  upgrwlkupwlk  42250  sprsymrelfolem2  42272  nrhmzr  42402  rngccatidALTV  42518  funcrngcsetcALT  42528  ringccatidALTV  42581  lincdifsn  42742  lindslinindimp2lem1  42776  lindsrng01  42786  ldepsnlinc  42826  m1modmmod  42845  blen1b  42911  nn0sumshdiglemB  42943  nn0sumshdiglem1  42944
  Copyright terms: Public domain W3C validator