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  810  impsingle  1623  meredith  1637  stdpc4  2065  ax12  2425  ax12vALT  2471  nfsb4t  2501  moexexlem  2623  pm2.61da3ne  3028  ralrimivw  3147  rexlimdvw  3157  reximdv  3167  vtocl2d  3561  reuind  3761  reuan  3904  2reu4  4528  rabeqsnd  4673  tppreqb  4809  ssprsseq  4829  n0snor2el  4837  prnebg  4860  prel12g  4868  elpreqprlem  4870  3elpr2eq  4910  disjord  5136  disjiund  5138  dtruALT2  5375  exneq  5445  dtruOLD  5451  propssopi  5517  opthhausdorff  5526  fr0  5666  ssrel2  5797  poltletr  6154  reuop  6314  ordsssuc2  6476  ordnbtwn  6478  ndmfv  6941  fveqres  6953  fmptco  7148  funsndifnop  7170  tpres  7220  fntpb  7228  elunirn  7270  isof1oopb  7344  fvmptopabOLD  7487  ndmovord  7622  ordsucelsuc  7841  tfinds  7880  tfindsg  7881  limomss  7891  findsg  7919  finds1  7921  xpexr  7940  bropopvvv  8113  bropfvvvvlem  8114  bropfvvvv  8115  soxp  8152  poseq  8181  suppun  8207  extmptsuppeq  8211  funsssuppss  8213  suppss  8217  suppss2  8223  suppssfv  8225  suppco  8229  mpoxopynvov0  8241  smofvon2  8394  oaordi  8582  oawordeulem  8590  odi  8615  omeulem1  8618  brdomg  8995  brdomgOLD  8996  snmapen  9076  fopwdom  9118  fodomr  9166  mapxpen  9181  infensuc  9193  onomeneqOLD  9263  fineqvlem  9295  fineqv  9296  xpfiOLD  9356  fodomfir  9365  finsschain  9396  fsuppun  9424  fsuppunbi  9426  funsnfsupp  9429  dffi3  9468  fisup2g  9505  fisupcl  9506  fiinf2g  9537  infsupprpr  9541  wemapso2  9590  epnsym  9646  en3lplem2  9650  preleqg  9652  inf3lemd  9664  r1ordg  9815  r1val1  9823  r1pw  9882  r1pwALT  9883  rankxplim3  9918  eldju2ndl  9961  eldju2ndr  9962  carddomi2  10007  fidomtri  10030  pr2neOLD  10042  alephon  10106  alephcard  10107  alephnbtwn  10108  alephordi  10111  iunfictbso  10151  fin23lem30  10379  fin1a2lem10  10446  axdc3lem2  10488  axdc3lem4  10490  alephval2  10609  cfpwsdom  10621  axextnd  10628  axrepnd  10631  axpownd  10638  axregnd  10641  axinfndlem1  10642  fpwwe2lem11  10678  wunfi  10758  addnidpi  10938  pinq  10964  mulgt0sr  11142  dedekind  11421  nnind  12281  nn1m1nn  12284  nn0n0n1ge2b  12592  nn0lt2  12678  nn0le2is012  12679  uzm1  12913  uzinfi  12967  nn01to3  12980  xrltnsym  13175  xrlttri  13177  xrlttr  13178  qbtwnxr  13238  xltnegi  13254  xnn0xaddcl  13273  xlt2add  13298  xrsupsslem  13345  xrinfmsslem  13346  xrub  13350  reltxrnmnf  13380  fzdif1  13641  fzospliti  13727  elfzonlteqm1  13776  fzoopth  13797  elfznelfzo  13807  injresinjlem  13822  injresinj  13823  modfzo0difsn  13980  addmodlteq  13983  ssnn0fi  14022  fsuppmapnn0fiub0  14030  suppssfz  14031  seqfveq2  14061  monoord  14069  seqf1o  14080  seqhomo  14086  expnngt1  14276  faclbnd4lem4  14331  hasheqf1oi  14386  hashrabsn1  14409  hashgt0elex  14436  hash1snb  14454  hashf1lem2  14491  hashf1  14492  seqcoll  14499  hashle2pr  14512  pr2pwpr  14514  hashge2el2difr  14516  swrdnnn0nd  14690  swrdnd0  14691  pfxnd0  14722  swrdswrd  14739  pfxccatin12lem3  14766  pfxccat3  14768  swrdccat3blem  14773  repsdf2  14812  repswsymballbi  14814  cshw0  14828  cshwmodn  14829  cshwn  14831  cshwcl  14832  cshwlen  14833  cshw1  14856  2cshwcshw  14860  cshimadifsn  14864  s3sndisj  15002  s3iunsndisj  15003  relexprelg  15073  relexpnndm  15076  relexpaddg  15088  relexpaddd  15089  rtrclreclem4  15096  relexpindlem  15098  rexuz3  15383  rexanuz2  15384  limsupgre  15513  rlimconst  15576  caurcvg  15709  caucvg  15711  sumss  15756  fsumcl2lem  15763  modfsummods  15825  fsumrlim  15843  fsumo1  15844  fprodcl2lem  15982  dvdsaddre2b  16340  dvdsabseq  16346  mod2eq1n2dvds  16380  nno  16415  sumeven  16420  sumodd  16421  nn0rppwr  16594  nn0seqcvgd  16603  lcmdvds  16641  lcmfunsnlem2  16673  lcmfunsnlem  16674  divgcdcoprm0  16698  ge2nprmge4  16734  exprmfct  16737  rpexp1i  16756  prm23lt5  16847  prm23ge5  16848  pcz  16914  pcadd  16922  pcmptcl  16924  oddprmdvds  16936  prmgaplem6  17089  prmgaplem7  17090  cshwshashlem1  17129  cshwsdisj  17132  prmlem0  17139  setsstruct  17209  ressress  17293  initoeu2lem2  18068  mgm2nsgrplem2  18944  mgm2nsgrplem3  18945  dfgrp2e  18993  dfgrp3e  19070  cyccom  19233  symgextf1  19453  gsmsymgrfix  19460  gsmsymgreq  19464  sylow1lem1  19630  efgsf  19761  efgrelexlema  19781  dprdss  20063  ablfac1eulem  20106  01eq0ringOLD  20547  nrhmzr  20553  funcrngcsetcALT  20657  lssssr  20969  psgnodpm  21623  psrvscafval  21985  mplcoe1  22072  mplcoe5  22075  mpfrcl  22126  mamudm  22414  matmulcell  22466  dmatmul  22518  scmatsgrp1  22543  mavmuldm  22571  mavmulsolcl  22572  mdetunilem9  22641  cramerlem3  22710  cramer0  22711  chpscmatgsumbin  22865  chp0mat  22867  fvmptnn04ifc  22873  fvmptnn04ifd  22874  epttop  23031  neiptopnei  23155  fiuncmp  23427  1stcrest  23476  kgenss  23566  hmeofval  23781  fbun  23863  fgss2  23897  filuni  23908  filssufilg  23934  filufint  23943  hausflimi  24003  hausflim  24004  hauspwpwf1  24010  fclscmp  24053  alexsubALTlem4  24073  ptcmplem3  24077  ptcmplem5  24079  cstucnd  24308  isxmet2d  24352  imasdsf1olem  24398  blfps  24431  blf  24432  metrest  24552  nrginvrcn  24728  nmoge0  24757  nmoleub  24767  fsumcn  24907  cmetcaulem  25335  iscmet3  25340  iscmet2  25341  bcthlem2  25372  ovolicc2lem3  25567  itg2seq  25791  itg2splitlem  25797  itgeq1fOLD  25821  itgeq2  25827  iblcnlem  25838  itgfsum  25876  limcnlp  25927  perfdvf  25952  dvnres  25981  dvmptfsum  26027  c1lip1  26050  dvply2g  26340  taylply2  26423  abelth  26499  cxpsqrtth  26786  rlimcnp  27022  xrlimcnp  27025  jensen  27046  ppiublem1  27260  dchrelbas3  27296  bcmono  27335  zabsle1  27354  gausslemma2dlem0f  27419  gausslemma2dlem1a  27423  gausslemma2dlem4  27427  lgsquad2lem2  27443  2lgslem1a1  27447  2lgslem3  27462  2lgs  27465  2lgsoddprm  27474  2sqlem10  27486  2sqnn  27497  addsqnreup  27501  2sqreultblem  27506  2sqreunnltblem  27509  pntrsumbnd2  27625  pntpbnd1  27644  pntlem3  27667  nolesgn2o  27730  noetalem1  27800  bday0b  27889  leftf  27918  rightf  27919  addscutlem  28024  negscut  28085  mulscutlem  28171  n0s0suc  28359  n0s0m1  28373  axcontlem7  28999  elntg2  29014  ausgrusgrb  29196  usgredg2v  29258  lfuhgr1v0e  29285  subumgredg2  29316  upgrreslem  29335  umgrreslem  29336  fusgrfisbase  29359  nbuhgr  29374  uhgrnbgr0nb  29385  nbgr0edglem  29387  nbgr1vtx  29389  cusgredg  29455  cusgrsizeinds  29484  sizusglecusg  29495  finsumvtxdg2size  29582  ewlkle  29637  upgriswlk  29673  pthdivtx  29761  usgr2trlncl  29792  crctcshwlkn0lem4  29842  wwlksn  29866  iswwlksnon  29882  iswspthsnon  29885  wwlksm1edg  29910  wwlksnfi  29935  2pthdlem1  29959  umgr2wlk  29978  umgrclwwlkge2  30019  clwlkclwwlklem2a  30026  clwlkclwwlk  30030  clwlkclwwlkf1lem2  30033  clwlkclwwlkf  30036  clwwisshclwws  30043  clwwlknlbonbgr1  30067  clwwlknon0  30121  clwwlknonel  30123  clwwlknonex2e  30138  3pthdlem1  30192  eupth2  30267  nfrgr2v  30300  frgr3vlem1  30301  1to2vfriswmgr  30307  1to3vfriswmgr  30308  vdgn1frgrv2  30324  frgrncvvdeqlem9  30335  frgrwopreglem4a  30338  frgrregorufr0  30352  frgrregorufr  30353  2wspmdisj  30365  2clwwlk2clwwlklem  30374  frgrreggt1  30421  frgrreg  30422  frgrregord13  30424  aevdemo  30488  shsvs  31351  0cnop  32007  0cnfn  32008  cnlnssadj  32108  ssmd1  32339  ssmd2  32340  atexch  32409  mdsymlem4  32434  sumdmdlem  32446  ifeqeqx  32562  fmptcof2  32673  padct  32736  nnindf  32825  drng0mxidl  33483  constr01  33746  pwsiga  34110  pwldsys  34137  ldsysgenld  34140  fiunelros  34154  breprexp  34626  bnj151  34869  bnj594  34904  bnj600  34911  subfacp1lem6  35169  erdszelem8  35182  cvmliftlem7  35275  cvmliftlem10  35278  cvmlift2lem12  35298  sat1el2xp  35363  mrsubfval  35492  msubfval  35508  mclsssvlem  35546  funpartfv  35926  endofsegid  36066  broutsideof2  36103  a1i24  36283  nn0prpwlem  36304  nn0prpw  36305  ordcmp  36429  findreccl  36435  bj-ax6e  36650  bj-ax12v3ALT  36668  bj-xpnzex  36941  bj-ideqg1  37146  rdgssun  37360  finxp00  37384  domalom  37386  isinf2  37387  fvineqsneq  37394  wl-spae  37501  wl-nfs1t  37517  poimirlem27  37633  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  itg2addnclem3  37659  itg2addnc  37660  ftc1anc  37687  areacirclem1  37694  sdclem2  37728  fdc  37731  mettrifi  37743  isexid2  37841  zerdivemp1x  37933  smprngopr  38038  mpobi123f  38148  mptbi12f  38152  ac6s6  38158  relcnveq3  38302  mopickr  38344  elrelscnveq3  38472  disjlem14  38779  jca3  38837  ax12fromc15  38886  hbequid  38890  dvelimf-o  38910  ax12eq  38922  ax12el  38923  ax12indalem  38926  ax12inda2ALT  38927  ax12inda2  38928  lfl1dim  39102  lfl1dim2N  39103  lkreqN  39151  cvrexchlem  39401  ps-2  39460  paddasslem14  39815  idldil  40096  isltrn2N  40102  cdleme25a  40335  dibglbN  41148  dihlsscpre  41216  dvh4dimlem  41425  lcfl7N  41483  mapdval2N  41612  dvrelog2b  42047  aks6d1c6lem3  42153  monotoddzzfi  42930  onov0suclim  43263  onmcl  43320  omabs2  43321  tfsconcat0b  43335  naddgeoa  43383  rp-fakeimass  43501  clublem  43599  grur1cld  44227  ee121  44502  ee122  44503  rspsbc2  44531  ax6e2ndeq  44556  vd12  44597  vd13  44598  ee221  44647  ee212  44649  ee112  44652  ee211  44655  ee210  44657  ee201  44659  ee120  44661  ee021  44663  ee012  44665  ee102  44667  ee03  44738  ee31  44749  ee31an  44751  ee123  44760  ax6e2ndeqVD  44906  ax6e2ndeqALT  44928  refsum2cnlem1  44974  fiiuncl  45004  eliin2f  45043  disjrnmpt2  45130  disjinfi  45134  rnmptbdlem  45199  allbutfi  45342  infxrunb3rnmpt  45377  infrpgernmpt  45414  monoordxrv  45431  mccl  45553  constlimc  45579  limclner  45606  xlimmnfvlem1  45787  xlimpnfvlem1  45791  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnprodlem3  45903  stoweidlem31  45986  pwsal  46270  prsal  46273  sge0pnffigt  46351  sge0ltfirp  46355  0ome  46484  hoicvrrex  46511  hoidmvle  46555  ovnhoilem1  46556  ovnlecvr2  46565  smflimlem3  46728  funressnfv  46992  euoreqb  47058  ndmaovass  47155  afv2orxorb  47177  otiunsndisjX  47228  nltle2tri  47262  smonoord  47295  iccpartigtl  47347  icceuelpartlem  47359  iccpartnel  47362  sprsymrelfolem2  47417  prproropf1olem4  47430  paireqne  47435  reupr  47446  reuopreuprim  47450  fmtnoprmfac1  47489  fmtnoprmfac2  47491  prmdvdsfmtnof1lem2  47509  31prm  47521  lighneallem3  47531  lighneallem4b  47533  lighneallem4  47534  lighneal  47535  nn0o1gt2ALTV  47618  nn0oALTV  47620  odd2prm2  47642  even3prm2  47643  fpprwppr  47663  stgoldbwt  47700  sbgoldbwt  47701  sbgoldbalt  47705  sbgoldbo  47711  nnsum3primesgbe  47716  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  bgoldbachlt  47737  tgblthelfgott  47739  dfclnbgr6  47779  grimco  47817  uhgrimisgrgric  47836  grtriprop  47845  usgrgrtrirex  47852  isubgr3stgrlem6  47873  isubgr3stgrlem8  47875  grlimgrtri  47898  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  gpgcubic  47969  gpg5nbgr3star  47971  upgrwlkupwlk  47983  rngccatidALTV  48115  ringccatidALTV  48149  lincdifsn  48269  lindslinindimp2lem1  48303  lindsrng01  48313  ldepsnlinc  48353  m1modmmod  48370  blen1b  48437  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  reorelicc  48559  rrx2xpref1o  48567  rrx2plord2  48571  rrxlinesc  48584  line2ylem  48600  line2xlem  48602  thincmon  48833  thincepi  48834