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

Step	Hyp	Ref	Expression
1		a1d.1	. 2 ⊢ (𝜑 → 𝜓)
2		ax-1 6	. 2 ⊢ (𝜓 → (𝜒 → 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 → 𝜓))

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  121  pm2.24d  151  conax1k  171  pm2.521g2  175  pm2.61iii  185  mtod  198  imbi2d  340  adantr  480  jctild  525  jctird  526  anbi2d  630  anbi1d  631  pm3.4  809  impsingle  1628  meredith  1642  stdpc4  2071  ax12  2423  ax12vALT  2469  nfsb4t  2499  moexexlem  2621  pm2.61da3ne  3017  ralrimivw  3128  rexlimdvw  3138  reximdv  3147  vtocl2d  3517  reuind  3712  reuan  3847  2reu4  4473  rabeqsnd  4622  tppreqb  4757  ssprsseq  4777  n0snor2el  4785  prnebg  4808  prel12g  4816  elpreqprlem  4818  3elpr2eq  4858  disjord  5080  disjiund  5082  dtruALT2  5308  exneq  5378  propssopi  5448  opthhausdorff  5457  fr0  5594  ssrel2  5725  poltletr  6079  reuop  6240  ordsssuc2  6399  ordnbtwn  6401  ndmfv  6854  fveqres  6866  fmptco  7062  funsndifnop  7084  tpres  7135  fntpb  7143  elunirn  7185  isof1oopb  7259  ndmovord  7536  ordsucelsuc  7752  tfinds  7790  tfindsg  7791  limomss  7801  findsg  7827  finds1  7829  xpexr  7848  resf1extb  7864  bropopvvv  8020  bropfvvvvlem  8021  bropfvvvv  8022  soxp  8059  poseq  8088  suppun  8114  extmptsuppeq  8118  funsssuppss  8120  suppss  8124  suppss2  8130  suppssfv  8132  suppco  8136  mpoxopynvov0  8148  smofvon2  8276  oaordi  8461  oawordeulem  8469  odi  8494  omeulem1  8497  brdomg  8881  snmapen  8960  fopwdom  8998  fodomr  9041  mapxpen  9056  infensuc  9068  fineqvlem  9150  fineqv  9151  fodomfir  9212  finsschain  9243  fsuppun  9271  fsuppunbi  9273  funsnfsupp  9276  dffi3  9315  fisup2g  9353  fisupcl  9354  fiinf2g  9386  infsupprpr  9390  wemapso2  9439  epnsym  9499  en3lplem2  9503  preleqg  9505  inf3lemd  9517  r1ordg  9668  r1val1  9676  r1pw  9735  r1pwALT  9736  rankxplim3  9771  eldju2ndl  9814  eldju2ndr  9815  carddomi2  9860  fidomtri  9883  alephon  9957  alephcard  9958  alephnbtwn  9959  alephordi  9962  iunfictbso  10002  fin23lem30  10230  fin1a2lem10  10297  axdc3lem2  10339  axdc3lem4  10341  alephval2  10460  cfpwsdom  10472  axextnd  10479  axrepnd  10482  axpownd  10489  axregnd  10492  axinfndlem1  10493  fpwwe2lem11  10529  wunfi  10609  addnidpi  10789  pinq  10815  mulgt0sr  10993  dedekind  11273  nnind  12140  nn1m1nn  12143  nn0n0n1ge2b  12447  nn0lt2  12533  nn0le2is012  12534  uzm1  12767  uzinfi  12823  nn01to3  12836  xrltnsym  13033  xrlttri  13035  xrlttr  13036  qbtwnxr  13096  xltnegi  13112  xnn0xaddcl  13131  xlt2add  13156  xrsupsslem  13203  xrinfmsslem  13204  xrub  13208  reltxrnmnf  13239  fzdif1  13502  fzospliti  13588  elfzonlteqm1  13638  fzoopth  13659  elfznelfzo  13670  injresinjlem  13687  injresinj  13688  modfzo0difsn  13847  addmodlteq  13850  ssnn0fi  13889  fsuppmapnn0fiub0  13897  suppssfz  13898  seqfveq2  13928  monoord  13936  seqf1o  13947  seqhomo  13953  expnngt1  14145  faclbnd4lem4  14200  hasheqf1oi  14255  hashrabsn1  14278  hashgt0elex  14305  hash1snb  14323  hashf1lem2  14360  hashf1  14361  seqcoll  14368  hashle2pr  14381  pr2pwpr  14383  hashge2el2difr  14385  swrdnnn0nd  14561  swrdnd0  14562  pfxnd0  14593  swrdswrd  14609  pfxccatin12lem3  14636  pfxccat3  14638  swrdccat3blem  14643  repsdf2  14682  repswsymballbi  14684  cshw0  14698  cshwmodn  14699  cshwn  14701  cshwcl  14702  cshwlen  14703  cshw1  14726  2cshwcshw  14729  cshimadifsn  14733  s3sndisj  14871  s3iunsndisj  14872  relexprelg  14942  relexpnndm  14945  relexpaddg  14957  relexpaddd  14958  rtrclreclem4  14965  relexpindlem  14967  rexuz3  15253  rexanuz2  15254  limsupgre  15385  rlimconst  15448  caurcvg  15581  caucvg  15583  sumss  15628  fsumcl2lem  15635  modfsummods  15697  fsumrlim  15715  fsumo1  15716  fprodcl2lem  15854  dvdsaddre2b  16215  dvdsabseq  16221  mod2eq1n2dvds  16255  nno  16290  sumeven  16295  sumodd  16296  nn0rppwr  16469  nn0seqcvgd  16478  lcmdvds  16516  lcmfunsnlem2  16548  lcmfunsnlem  16549  divgcdcoprm0  16573  ge2nprmge4  16609  exprmfct  16612  rpexp1i  16631  prm23lt5  16723  prm23ge5  16724  pcz  16790  pcadd  16798  pcmptcl  16800  oddprmdvds  16812  prmgaplem6  16965  prmgaplem7  16966  cshwshashlem1  17004  cshwsdisj  17007  prmlem0  17014  setsstruct  17084  ressress  17155  initoeu2lem2  17919  mgm2nsgrplem2  18824  mgm2nsgrplem3  18825  dfgrp2e  18873  dfgrp3e  18950  cyccom  19113  symgextf1  19331  gsmsymgrfix  19338  gsmsymgreq  19342  sylow1lem1  19508  efgsf  19639  efgrelexlema  19659  dprdss  19941  ablfac1eulem  19984  01eq0ringOLD  20444  nrhmzr  20450  funcrngcsetcALT  20554  lssssr  20885  psgnodpm  21523  psrvscafval  21883  mplcoe1  21970  mplcoe5  21973  mpfrcl  22018  mamudm  22308  matmulcell  22358  dmatmul  22410  scmatsgrp1  22435  mavmuldm  22463  mavmulsolcl  22464  mdetunilem9  22533  cramerlem3  22602  cramer0  22603  chpscmatgsumbin  22757  chp0mat  22759  fvmptnn04ifc  22765  fvmptnn04ifd  22766  epttop  22922  neiptopnei  23045  fiuncmp  23317  1stcrest  23366  kgenss  23456  hmeofval  23671  fbun  23753  fgss2  23787  filuni  23798  filssufilg  23824  filufint  23833  hausflimi  23893  hausflim  23894  hauspwpwf1  23900  fclscmp  23943  alexsubALTlem4  23963  ptcmplem3  23967  ptcmplem5  23969  cstucnd  24196  isxmet2d  24240  imasdsf1olem  24286  blfps  24319  blf  24320  metrest  24437  nrginvrcn  24605  nmoge0  24634  nmoleub  24644  fsumcn  24786  cmetcaulem  25213  iscmet3  25218  iscmet2  25219  bcthlem2  25250  ovolicc2lem3  25445  itg2seq  25668  itg2splitlem  25674  itgeq1fOLD  25698  itgeq2  25704  iblcnlem  25715  itgfsum  25753  limcnlp  25804  perfdvf  25829  dvnres  25858  dvmptfsum  25904  c1lip1  25927  dvply2g  26217  taylply2  26300  abelth  26376  cxpsqrtth  26664  rlimcnp  26900  xrlimcnp  26903  jensen  26924  ppiublem1  27138  dchrelbas3  27174  bcmono  27213  zabsle1  27232  gausslemma2dlem0f  27297  gausslemma2dlem1a  27301  gausslemma2dlem4  27305  lgsquad2lem2  27321  2lgslem1a1  27325  2lgslem3  27340  2lgs  27343  2lgsoddprm  27352  2sqlem10  27364  2sqnn  27375  addsqnreup  27379  2sqreultblem  27384  2sqreunnltblem  27387  pntrsumbnd2  27503  pntpbnd1  27522  pntlem3  27545  nolesgn2o  27608  noetalem1  27678  bday0b  27772  leftf  27808  rightf  27809  oldss  27821  addscutlem  27918  negscut  27979  mulscutlem  28068  n0s0suc  28268  n0sfincut  28280  n0s0m1  28286  nn1m1nns  28297  axcontlem7  28946  elntg2  28961  ausgrusgrb  29141  usgredg2v  29203  lfuhgr1v0e  29230  subumgredg2  29261  upgrreslem  29280  umgrreslem  29281  fusgrfisbase  29304  nbuhgr  29319  uhgrnbgr0nb  29330  nbgr0edglem  29332  nbgr1vtx  29334  cusgredg  29400  cusgrsizeinds  29429  sizusglecusg  29440  finsumvtxdg2size  29527  ewlkle  29582  upgriswlk  29617  pthdivtx  29703  dfpth2  29705  usgr2trlncl  29736  crctcshwlkn0lem4  29789  wwlksn  29813  iswwlksnon  29829  iswspthsnon  29832  wwlksm1edg  29857  wwlksnfi  29882  2pthdlem1  29906  umgr2wlk  29925  umgrclwwlkge2  29966  clwlkclwwlklem2a  29973  clwlkclwwlk  29977  clwlkclwwlkf1lem2  29980  clwlkclwwlkf  29983  clwwisshclwws  29990  clwwlknlbonbgr1  30014  clwwlknon0  30068  clwwlknonel  30070  clwwlknonex2e  30085  3pthdlem1  30139  eupth2  30214  nfrgr2v  30247  frgr3vlem1  30248  1to2vfriswmgr  30254  1to3vfriswmgr  30255  vdgn1frgrv2  30271  frgrncvvdeqlem9  30282  frgrwopreglem4a  30285  frgrregorufr0  30299  frgrregorufr  30300  2wspmdisj  30312  2clwwlk2clwwlklem  30321  frgrreggt1  30368  frgrreg  30369  frgrregord13  30371  aevdemo  30435  shsvs  31298  0cnop  31954  0cnfn  31955  cnlnssadj  32055  ssmd1  32286  ssmd2  32287  atexch  32356  mdsymlem4  32381  sumdmdlem  32393  ifeqeqx  32517  fmptcof2  32634  padct  32696  nnindf  32797  drng0mxidl  33436  constr01  33750  pwsiga  34138  pwldsys  34165  ldsysgenld  34168  fiunelros  34182  breprexp  34641  bnj151  34884  bnj594  34919  bnj600  34926  trssfir1omregs  35120  subfacp1lem6  35217  erdszelem8  35230  cvmliftlem7  35323  cvmliftlem10  35326  cvmlift2lem12  35346  sat1el2xp  35411  mrsubfval  35540  msubfval  35556  mclsssvlem  35594  antnestlaw2  35724  funpartfv  35978  endofsegid  36118  broutsideof2  36155  a1i24  36334  nn0prpwlem  36355  nn0prpw  36356  ordcmp  36480  findreccl  36486  bj-ax6e  36701  bj-ax12v3ALT  36719  bj-xpnzex  36992  bj-ideqg1  37197  rdgssun  37411  finxp00  37435  domalom  37437  isinf2  37438  fvineqsneq  37445  wl-spae  37554  wl-nfs1t  37570  poimirlem27  37686  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  itg2addnclem3  37712  itg2addnc  37713  ftc1anc  37740  areacirclem1  37747  sdclem2  37781  fdc  37784  mettrifi  37796  isexid2  37894  zerdivemp1x  37986  smprngopr  38091  mpobi123f  38201  mptbi12f  38205  ac6s6  38211  relcnveq3  38354  mopickr  38390  elrelscnveq3  38527  disjlem14  38835  jca3  38894  ax12fromc15  38943  hbequid  38947  dvelimf-o  38967  ax12eq  38979  ax12el  38980  ax12indalem  38983  ax12inda2ALT  38984  ax12inda2  38985  lfl1dim  39159  lfl1dim2N  39160  lkreqN  39208  cvrexchlem  39457  ps-2  39516  paddasslem14  39871  idldil  40152  isltrn2N  40158  cdleme25a  40391  dibglbN  41204  dihlsscpre  41272  dvh4dimlem  41481  lcfl7N  41539  mapdval2N  41668  dvrelog2b  42098  aks6d1c6lem3  42204  monotoddzzfi  42974  onov0suclim  43306  onmcl  43363  omabs2  43364  tfsconcat0b  43378  naddgeoa  43426  rp-fakeimass  43544  clublem  43642  grur1cld  44264  ee121  44537  ee122  44538  rspsbc2  44566  ax6e2ndeq  44591  vd12  44632  vd13  44633  ee221  44682  ee212  44684  ee112  44687  ee211  44690  ee210  44692  ee201  44694  ee120  44696  ee021  44698  ee012  44700  ee102  44702  ee03  44772  ee31  44783  ee31an  44785  ee123  44794  ax6e2ndeqVD  44940  ax6e2ndeqALT  44962  refsum2cnlem1  45073  fiiuncl  45101  eliin2f  45140  disjrnmpt2  45224  disjinfi  45228  rnmptbdlem  45291  allbutfi  45430  infxrunb3rnmpt  45465  infrpgernmpt  45502  monoordxrv  45518  mccl  45637  constlimc  45663  limclner  45688  xlimmnfvlem1  45869  xlimpnfvlem1  45873  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvnprodlem3  45985  stoweidlem31  46068  pwsal  46352  prsal  46355  sge0pnffigt  46433  sge0ltfirp  46437  0ome  46566  hoicvrrex  46593  hoidmvle  46637  ovnhoilem1  46638  ovnlecvr2  46647  smflimlem3  46810  ormkglobd  46912  funressnfv  47073  euoreqb  47139  ndmaovass  47236  afv2orxorb  47258  otiunsndisjX  47309  nltle2tri  47343  m1modmmod  47388  smonoord  47401  iccpartigtl  47453  icceuelpartlem  47465  iccpartnel  47468  sprsymrelfolem2  47523  prproropf1olem4  47536  paireqne  47541  reupr  47552  reuopreuprim  47556  fmtnoprmfac1  47595  fmtnoprmfac2  47597  prmdvdsfmtnof1lem2  47615  31prm  47627  lighneallem3  47637  lighneallem4b  47639  lighneallem4  47640  lighneal  47641  nn0o1gt2ALTV  47724  nn0oALTV  47726  odd2prm2  47748  even3prm2  47749  fpprwppr  47769  stgoldbwt  47806  sbgoldbwt  47807  sbgoldbalt  47811  sbgoldbo  47817  nnsum3primesgbe  47822  wtgoldbnnsum4prm  47832  bgoldbnnsum3prm  47834  bgoldbtbndlem2  47836  bgoldbtbndlem3  47837  bgoldbtbndlem4  47838  bgoldbtbnd  47839  bgoldbachlt  47843  tgblthelfgott  47845  dfclnbgr6  47886  grimco  47919  uhgrimisgrgric  47961  grtriprop  47971  usgrgrtrirex  47980  isubgr3stgrlem6  48001  isubgr3stgrlem8  48003  grlimprclnbgr  48026  grlimgrtri  48033  gpgedg2ov  48096  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem2  48102  gpg5nbgrvtx13starlem3  48103  gpgcubic  48109  gpg5nbgr3star  48111  gpgprismgr4cycllem7  48131  pgnbgreunbgrlem2  48147  gpg5edgnedg  48160  upgrwlkupwlk  48170  rngccatidALTV  48302  ringccatidALTV  48336  lincdifsn  48455  lindslinindimp2lem1  48489  lindsrng01  48499  ldepsnlinc  48539  blen1b  48619  nn0sumshdiglemB  48651  nn0sumshdiglem1  48652  reorelicc  48741  rrx2xpref1o  48749  rrx2plord2  48753  rrxlinesc  48766  line2ylem  48782  line2xlem  48784  thincmon  49464  thincepi  49465