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  118  pm2.24d  147  pm2.51  165  pm2.521  166  pm2.61iii  179  mtod  189  impbid21d  201  imbi2d  330  adantr  481  jctild  565  jctird  566  pm3.4  583  anbi2d  739  anbi1d  740  ad4ant13  1289  ad4ant134  1293  meredith  1563  ax12  2303  ax12OLD  2340  nfsb4t  2388  ax12vALT  2427  moexex  2540  pm2.61da3ne  2879  ralrimivw  2963  reximdv  3012  rexlimdvw  3029  reuind  3398  sbcimdvOLD  3486  rexn0  4052  eqoreldifOLD  4204  tppreqb  4312  ssprsseq  4332  n0snor2el  4339  prnebg  4364  elpreqprlem  4370  axsep  4750  dtru  4827  propeqop  4940  propssopi  4941  fr0  5063  ssrel2  5181  poltletr  5497  ordsssuc2  5783  ordnbtwn  5785  ndmfv  6185  fveqres  6197  fmptco  6362  funsndifnop  6381  tpres  6431  fntpb  6438  elunirn  6474  isof1oopb  6540  fvmptopab  6662  ndmovord  6789  abnex  6929  ordsucelsuc  6984  tfinds  7021  tfindsg  7022  limomss  7032  findsg  7055  finds1  7057  xpexr  7068  bropopvvv  7215  bropfvvvvlem  7216  bropfvvvv  7217  soxp  7250  suppun  7275  extmptsuppeq  7279  funsssuppss  7281  suppss  7285  suppssov1  7287  suppss2  7289  suppssfv  7291  mpt2xopynvov0  7304  smofvon2  7413  oaordi  7586  oawordeulem  7594  odi  7619  brdomg  7925  map1  7996  fopwdom  8028  fodomr  8071  mapxpen  8086  infensuc  8098  onomeneq  8110  fineqvlem  8134  fineqv  8135  xpfi  8191  finsschain  8233  fsuppun  8254  fsuppunbi  8256  funsnfsupp  8259  dffi3  8297  fisup2g  8334  fisupcl  8335  fiinf2g  8366  wemapso2  8418  en3lplem2  8472  inf3lemd  8484  r1ordg  8601  r1val1  8609  r1pw  8668  r1pwALT  8669  rankxplim3  8704  carddomi2  8756  fidomtri  8779  pr2ne  8788  alephon  8852  alephcard  8853  alephnbtwn  8854  alephordi  8857  iunfictbso  8897  fin23lem30  9124  fin1a2lem10  9191  axdc3lem2  9233  axdc3lem4  9235  alephval2  9354  cfpwsdom  9366  axextnd  9373  axrepnd  9376  axpownd  9383  axregnd  9386  axinfndlem1  9387  fpwwe2lem12  9423  wunfi  9503  addnidpi  9683  pinq  9709  mulgt0sr  9886  dedekind  10160  nnind  10998  nn1m1nn  11000  nn0n0n1ge2b  11319  nn0lt2  11400  nn0le2is012  11401  uzm1  11678  uzinfi  11728  nn01to3  11741  xrltnsym  11930  xrlttri  11932  xrlttr  11933  qbtwnxr  11990  xltnegi  12006  xnn0xaddcl  12025  xlt2add  12049  xrsupsslem  12096  xrinfmsslem  12097  xrub  12101  reltxrnmnf  12130  fzospliti  12457  elfzonlteqm1  12500  elfznelfzo  12530  injresinjlem  12544  injresinj  12545  modfzo0difsn  12698  addmodlteq  12701  ssnn0fi  12740  fsuppmapnn0fiub0  12749  suppssfz  12750  seqfveq2  12779  seqshft2  12783  monoord  12787  seqsplit  12790  seqf1o  12798  seqhomo  12804  faclbnd4lem4  13039  hasheqf1oi  13096  hasheqf1oiOLD  13097  hashrabsn1  13119  hashgt0elex  13145  hash1snb  13163  hashf1lem2  13194  hashf1  13195  seqcoll  13202  hashle2pr  13213  pr2pwpr  13215  hashge2el2difr  13217  2swrd1eqwrdeq  13408  swrdswrd  13414  swrdccatin1  13436  swrdccatin12lem3  13443  swrdccat3  13445  swrdccat3blem  13448  repsdf2  13478  repswsymballbi  13480  cshw0  13493  cshwmodn  13494  cshwn  13496  cshwcl  13497  cshwlen  13498  cshw1  13521  2cshwcshw  13524  cshimadifsn  13528  s3sndisj  13656  s3iunsndisj  13657  relexprelg  13728  relexpnndm  13731  relexpaddg  13743  relexpaddd  13744  resqrex  13941  rexuz3  14038  rexanuz2  14039  limsupgre  14162  rlimconst  14225  caurcvg  14357  caucvg  14359  sumss  14404  fsumcl2lem  14411  modfsummods  14471  fsumrlim  14489  fsumo1  14490  fprodcl2lem  14624  dvdsaddre2b  14972  dvdsabseq  14978  mod2eq1n2dvds  15014  nno  15041  sumeven  15053  sumodd  15054  nn0seqcvgd  15226  lcmdvds  15264  lcmfunsnlem2  15296  lcmfunsnlem  15297  divgcdcoprm0  15322  exprmfct  15359  rpexp1i  15376  prm23lt5  15462  prm23ge5  15463  pcz  15528  pcadd  15536  pcmptcl  15538  oddprmdvds  15550  prmgaplem5  15702  prmgaplem6  15703  prmgaplem7  15704  cshwshashlem1  15745  cshwsdisj  15748  prmlem0  15755  setsstruct  15838  ressress  15878  initoeu2lem2  16605  mgm2nsgrplem2  17346  mgm2nsgrplem3  17347  dfgrp2e  17388  dfgrp3e  17455  symgextf1  17781  gsmsymgrfix  17788  gsmsymgreq  17792  sylow1lem1  17953  efgsf  18082  efgrelexlema  18102  dprdss  18368  ablfac1eulem  18411  lssssr  18893  01eq0ring  19212  psrvscafval  19330  mplcoe1  19405  mplcoe5  19408  mpfrcl  19458  psgnodpm  19874  mamudm  20134  matmulcell  20191  dmatmul  20243  scmatsgrp1  20268  mavmuldm  20296  mavmulsolcl  20297  mdetunilem9  20366  cramerlem3  20435  cramer0  20436  chpscmatgsumbin  20589  chp0mat  20591  fvmptnn04ifc  20597  fvmptnn04ifd  20598  epttop  20753  neiptopnei  20876  fiuncmp  21147  1stcrest  21196  comppfsc  21275  kgenss  21286  hmeofval  21501  fbun  21584  fgss2  21618  filuni  21629  filssufilg  21655  filufint  21664  hausflimi  21724  hausflim  21725  hauspwpwf1  21731  fclscmp  21774  alexsubALTlem4  21794  ptcmplem3  21798  ptcmplem5  21800  cstucnd  22028  isxmet2d  22072  imasdsf1olem  22118  blfps  22151  blf  22152  metrest  22269  nrginvrcn  22436  nmoge0  22465  nmoleub  22475  fsumcn  22613  cmetcaulem  23026  iscmet3  23031  iscmet2  23032  bcthlem2  23062  ovolicc2lem3  23227  itg2seq  23449  itg2splitlem  23455  itgeq1f  23478  itgeq2  23484  iblcnlem  23495  itgfsum  23533  limcnlp  23582  perfdvf  23607  dvnres  23634  dvmptfsum  23676  c1lip1  23698  abelth  24133  sinq12ge0  24198  rlimcnp  24626  xrlimcnp  24629  jensen  24649  ppiublem1  24861  dchrelbas3  24897  bcmono  24936  zabsle1  24955  gausslemma2dlem0f  25020  gausslemma2dlem1a  25024  gausslemma2dlem4  25028  lgsquad2lem2  25044  2lgslem1a1  25048  2lgslem3  25063  2lgs  25066  2lgsoddprm  25075  2sqlem10  25087  pntrsumbnd2  25190  pntpbnd1  25209  pntlem3  25232  axcontlem7  25784  ausgrusgrb  25987  usgredg2v  26046  lfuhgr1v0e  26073  subumgredg2  26104  fusgrfisbase  26142  nbuhgr  26160  uhgrnbgr0nb  26171  nbgr0vtxlem  26172  nbgr1vtx  26175  uvtxa0  26215  uvtx2vtx1edg  26220  cusgredg  26241  cusgrsizeinds  26269  sizusglecusg  26280  ewlkle  26405  upgriswlk  26440  pthdivtx  26528  usgr2trlncl  26559  crctcshwlkn0lem4  26608  wwlksn  26632  iswwlksnon  26643  iswspthsnon  26644  wwlksm1edg  26670  wwlksnfi  26704  wwlksnonfi  26719  wspn0  26723  2pthdlem1  26729  umgr2wlk  26748  2wspdisj  26757  2wspiundisj  26758  clwwlksn  26782  clwlkclwwlklem2a  26800  clwlkclwwlk  26804  umgrclwwlksge2  26812  clwwlksnfi  26813  clwwisshclwws  26828  clwwnisshclwwsn  26830  3pthdlem1  26924  eupth2  26999  nfrgr2v  27034  frgr3vlem1  27035  1to2vfriswmgr  27041  1to3vfriswmgr  27042  vdgn1frgrv2  27058  frgrwopreglem3  27075  frgrwopreglem4  27076  frgrwopreg  27078  frgrregorufr0  27081  frgrregorufr  27082  fusgr2wsp2nb  27090  2wspmdisj  27093  numclwwlkovf2ex  27109  extwwlkfab  27112  frgrreggt1  27139  frgrreg  27140  frgrregord13  27142  aevdemo  27205  shsvs  28070  0cnop  28726  0cnfn  28727  cnlnssadj  28827  ssmd1  29058  ssmd2  29059  atexch  29128  mdsymlem4  29153  sumdmdlem  29165  rabeqsnd  29230  ifeqeqx  29249  fmptcof2  29340  padct  29381  nnindf  29448  pwsiga  30016  ldsysgenld  30046  fiunelros  30060  bnj151  30708  bnj594  30743  bnj600  30750  subfacp1lem6  30928  erdszelem8  30941  cvmliftlem7  31034  cvmliftlem10  31037  cvmlift2lem12  31057  mrsubfval  31166  msubfval  31182  mclsssvlem  31220  trpredlem1  31481  poseq  31504  funpartfv  31747  endofsegid  31887  broutsideof2  31924  a1i24  31990  nn0prpwlem  32012  nn0prpw  32013  ordcmp  32141  findreccl  32147  bj-alsb  32320  bj-ax6e  32348  bj-ax12v3ALT  32371  bj-axsep  32489  bj-dtru  32493  bj-xpnzex  32646  finxp00  32910  wl-spae  32977  wl-nfs1t  32995  poimirlem27  33107  ovoliunnfl  33122  voliunnfl  33124  volsupnfl  33125  itg2addnclem3  33134  itg2addnc  33135  ftc1anc  33164  areacirclem1  33171  sdclem2  33209  fdc  33212  mettrifi  33224  isexid2  33325  zerdivemp1x  33417  smprngopr  33522  mpt2bi123f  33642  mptbi12f  33646  ac6s6  33651  jca3  33657  ax12fromc15  33709  hbequid  33713  dvelimf-o  33733  ax12eq  33745  ax12el  33746  ax12indalem  33749  ax12inda2ALT  33750  ax12inda2  33751  lfl1dim  33927  lfl1dim2N  33928  lkreqN  33976  cvrexchlem  34224  ps-2  34283  paddasslem14  34638  idldil  34919  isltrn2N  34925  cdleme25a  35160  dibglbN  35974  dihlsscpre  36042  dvh4dimlem  36251  lcfl7N  36309  mapdval2N  36438  monotoddzzfi  37026  rp-fakeimass  37377  clublem  37437  relexpnul  37490  ee121  38232  ee122  38233  rspsbc2  38265  ax6e2ndeq  38296  vd12  38346  vd13  38347  ee221  38396  ee212  38398  ee112  38401  ee211  38404  ee210  38406  ee201  38408  ee120  38410  ee021  38412  ee012  38414  ee102  38416  ee03  38489  ee31  38500  ee31an  38502  ee123  38511  ax6e2ndeqVD  38667  ax6e2ndeqALT  38689  refsum2cnlem1  38718  fiiuncl  38756  eliin2f  38809  disjrnmpt2  38884  disjinfi  38889  rnmptbd2lem  38974  rnmptbdlem  38981  allbutfi  39115  infxrunb3rnmpt  39154  mccl  39266  constlimc  39292  limclner  39319  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvmptfprod  39497  dvnprodlem3  39500  stoweidlem31  39585  pwsal  39872  prsal  39875  sge0pnffigt  39950  sge0ltfirp  39954  0ome  40080  hoicvrrex  40107  hoidmvle  40151  ovnhoilem1  40152  ovnlecvr2  40161  smflimlem3  40318  reuan  40514  2reu4  40524  funressnfv  40542  ndmaovass  40620  otiunsndisjX  40625  nltle2tri  40650  fzoopth  40664  smonoord  40669  iccpartigtl  40687  icceuelpartlem  40699  iccpartnel  40702  pfxccat3  40755  fmtnoprmfac1  40806  fmtnoprmfac2  40808  prmdvdsfmtnof1lem2  40826  31prm  40841  lighneallem3  40853  lighneallem4b  40855  lighneallem4  40856  lighneal  40857  nn0o1gt2ALTV  40934  nn0oALTV  40936  stgoldbwt  40989  bgoldbwt  40990  sgoldbalt  40994  nnsum3primesgbe  40999  wtgoldbnnsum4prm  41009  bgoldbnnsum3prm  41011  bgoldbtbndlem2  41013  bgoldbtbndlem3  41014  bgoldbtbndlem4  41015  bgoldbtbnd  41016  bgoldbachlt  41018  tgblthelfgott  41020  bgoldbachltOLD  41025  tgblthelfgottOLD  41027  upgrwlkupwlk  41039  sprsymrelfolem2  41061  nrhmzr  41191  rngccatidALTV  41307  funcrngcsetcALT  41317  ringccatidALTV  41370  lincdifsn  41531  lindslinindimp2lem1  41565  lindsrng01  41575  ldepsnlinc  41615  m1modmmod  41634  blen1b  41704  nn0sumshdiglemB  41736  nn0sumshdiglem1  41737
  Copyright terms: Public domain W3C validator