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  2073  ax12  2425  ax12vALT  2471  nfsb4t  2501  moexexlem  2623  pm2.61da3ne  3018  ralrimivw  3129  rexlimdvw  3139  reximdv  3148  vtocl2d  3516  reuind  3708  reuan  3843  2reu4  4472  rabeqsnd  4621  tppreqb  4756  ssprsseq  4776  n0snor2el  4784  prnebg  4807  prel12g  4815  elpreqprlem  4817  3elpr2eq  4857  disjord  5082  disjiund  5084  dtruALT2  5310  exneq  5380  propssopi  5451  opthhausdorff  5460  fr0  5597  ssrel2  5729  poltletr  6083  reuop  6245  ordsssuc2  6404  ordnbtwn  6406  ndmfv  6860  fveqres  6872  fmptco  7068  funsndifnop  7090  tpres  7141  fntpb  7149  elunirn  7191  isof1oopb  7265  ndmovord  7542  ordsucelsuc  7758  tfinds  7796  tfindsg  7797  limomss  7807  findsg  7833  finds1  7835  xpexr  7854  resf1extb  7870  bropopvvv  8026  bropfvvvvlem  8027  bropfvvvv  8028  soxp  8065  poseq  8094  suppun  8120  extmptsuppeq  8124  funsssuppss  8126  suppss  8130  suppss2  8136  suppssfv  8138  suppco  8142  mpoxopynvov0  8154  smofvon2  8282  oaordi  8467  oawordeulem  8475  odi  8500  omeulem1  8503  brdomg  8887  snmapen  8967  fopwdom  9005  fodomr  9048  mapxpen  9063  infensuc  9075  fineqvlem  9157  fineqv  9158  fodomfir  9219  finsschain  9250  fsuppun  9278  fsuppunbi  9280  funsnfsupp  9283  dffi3  9322  fisup2g  9360  fisupcl  9361  fiinf2g  9393  infsupprpr  9397  wemapso2  9446  epnsym  9506  en3lplem2  9510  preleqg  9512  inf3lemd  9524  r1ordg  9678  r1val1  9686  r1pw  9745  r1pwALT  9746  rankxplim3  9781  eldju2ndl  9824  eldju2ndr  9825  carddomi2  9870  fidomtri  9893  alephon  9967  alephcard  9968  alephnbtwn  9969  alephordi  9972  iunfictbso  10012  fin23lem30  10240  fin1a2lem10  10307  axdc3lem2  10349  axdc3lem4  10351  alephval2  10470  cfpwsdom  10482  axextnd  10489  axrepnd  10492  axpownd  10499  axregnd  10502  axinfndlem1  10503  fpwwe2lem11  10539  wunfi  10619  addnidpi  10799  pinq  10825  mulgt0sr  11003  dedekind  11283  nnind  12150  nn1m1nn  12153  nn0n0n1ge2b  12457  nn0lt2  12542  nn0le2is012  12543  uzm1  12772  uzinfi  12828  nn01to3  12841  xrltnsym  13038  xrlttri  13040  xrlttr  13041  qbtwnxr  13101  xltnegi  13117  xnn0xaddcl  13136  xlt2add  13161  xrsupsslem  13208  xrinfmsslem  13209  xrub  13213  reltxrnmnf  13244  fzdif1  13507  fzospliti  13593  elfzonlteqm1  13643  fzoopth  13664  elfznelfzo  13675  injresinjlem  13692  injresinj  13693  modfzo0difsn  13852  addmodlteq  13855  ssnn0fi  13894  fsuppmapnn0fiub0  13902  suppssfz  13903  seqfveq2  13933  monoord  13941  seqf1o  13952  seqhomo  13958  expnngt1  14150  faclbnd4lem4  14205  hasheqf1oi  14260  hashrabsn1  14283  hashgt0elex  14310  hash1snb  14328  hashf1lem2  14365  hashf1  14366  seqcoll  14373  hashle2pr  14386  pr2pwpr  14388  hashge2el2difr  14390  swrdnnn0nd  14566  swrdnd0  14567  pfxnd0  14598  swrdswrd  14614  pfxccatin12lem3  14641  pfxccat3  14643  swrdccat3blem  14648  repsdf2  14687  repswsymballbi  14689  cshw0  14703  cshwmodn  14704  cshwn  14706  cshwcl  14707  cshwlen  14708  cshw1  14731  2cshwcshw  14734  cshimadifsn  14738  s3sndisj  14876  s3iunsndisj  14877  relexprelg  14947  relexpnndm  14950  relexpaddg  14962  relexpaddd  14963  rtrclreclem4  14970  relexpindlem  14972  rexuz3  15258  rexanuz2  15259  limsupgre  15390  rlimconst  15453  caurcvg  15586  caucvg  15588  sumss  15633  fsumcl2lem  15640  modfsummods  15702  fsumrlim  15720  fsumo1  15721  fprodcl2lem  15859  dvdsaddre2b  16220  dvdsabseq  16226  mod2eq1n2dvds  16260  nno  16295  sumeven  16300  sumodd  16301  nn0rppwr  16474  nn0seqcvgd  16483  lcmdvds  16521  lcmfunsnlem2  16553  lcmfunsnlem  16554  divgcdcoprm0  16578  ge2nprmge4  16614  exprmfct  16617  rpexp1i  16636  prm23lt5  16728  prm23ge5  16729  pcz  16795  pcadd  16803  pcmptcl  16805  oddprmdvds  16817  prmgaplem6  16970  prmgaplem7  16971  cshwshashlem1  17009  cshwsdisj  17012  prmlem0  17019  setsstruct  17089  ressress  17160  initoeu2lem2  17924  mgm2nsgrplem2  18829  mgm2nsgrplem3  18830  dfgrp2e  18878  dfgrp3e  18955  cyccom  19117  symgextf1  19335  gsmsymgrfix  19342  gsmsymgreq  19346  sylow1lem1  19512  efgsf  19643  efgrelexlema  19663  dprdss  19945  ablfac1eulem  19988  01eq0ringOLD  20448  nrhmzr  20454  funcrngcsetcALT  20558  lssssr  20889  psgnodpm  21527  psrvscafval  21887  mplcoe1  21973  mplcoe5  21976  mpfrcl  22021  mamudm  22311  matmulcell  22361  dmatmul  22413  scmatsgrp1  22438  mavmuldm  22466  mavmulsolcl  22467  mdetunilem9  22536  cramerlem3  22605  cramer0  22606  chpscmatgsumbin  22760  chp0mat  22762  fvmptnn04ifc  22768  fvmptnn04ifd  22769  epttop  22925  neiptopnei  23048  fiuncmp  23320  1stcrest  23369  kgenss  23459  hmeofval  23674  fbun  23756  fgss2  23790  filuni  23801  filssufilg  23827  filufint  23836  hausflimi  23896  hausflim  23897  hauspwpwf1  23903  fclscmp  23946  alexsubALTlem4  23966  ptcmplem3  23970  ptcmplem5  23972  cstucnd  24199  isxmet2d  24243  imasdsf1olem  24289  blfps  24322  blf  24323  metrest  24440  nrginvrcn  24608  nmoge0  24637  nmoleub  24647  fsumcn  24789  cmetcaulem  25216  iscmet3  25221  iscmet2  25222  bcthlem2  25253  ovolicc2lem3  25448  itg2seq  25671  itg2splitlem  25677  itgeq1fOLD  25701  itgeq2  25707  iblcnlem  25718  itgfsum  25756  limcnlp  25807  perfdvf  25832  dvnres  25861  dvmptfsum  25907  c1lip1  25930  dvply2g  26220  taylply2  26303  abelth  26379  cxpsqrtth  26667  rlimcnp  26903  xrlimcnp  26906  jensen  26927  ppiublem1  27141  dchrelbas3  27177  bcmono  27216  zabsle1  27235  gausslemma2dlem0f  27300  gausslemma2dlem1a  27304  gausslemma2dlem4  27308  lgsquad2lem2  27324  2lgslem1a1  27328  2lgslem3  27343  2lgs  27346  2lgsoddprm  27355  2sqlem10  27367  2sqnn  27378  addsqnreup  27382  2sqreultblem  27387  2sqreunnltblem  27390  pntrsumbnd2  27506  pntpbnd1  27525  pntlem3  27548  nolesgn2o  27611  noetalem1  27681  bday0b  27775  leftf  27811  rightf  27812  oldss  27824  addscutlem  27921  negscut  27982  mulscutlem  28071  n0s0suc  28271  n0sfincut  28283  n0s0m1  28289  nn1m1nns  28300  axcontlem7  28950  elntg2  28965  ausgrusgrb  29145  usgredg2v  29207  lfuhgr1v0e  29234  subumgredg2  29265  upgrreslem  29284  umgrreslem  29285  fusgrfisbase  29308  nbuhgr  29323  uhgrnbgr0nb  29334  nbgr0edglem  29336  nbgr1vtx  29338  cusgredg  29404  cusgrsizeinds  29433  sizusglecusg  29444  finsumvtxdg2size  29531  ewlkle  29586  upgriswlk  29621  pthdivtx  29707  dfpth2  29709  usgr2trlncl  29740  crctcshwlkn0lem4  29793  wwlksn  29817  iswwlksnon  29833  iswspthsnon  29836  wwlksm1edg  29861  wwlksnfi  29886  2pthdlem1  29910  umgr2wlk  29929  umgrclwwlkge2  29973  clwlkclwwlklem2a  29980  clwlkclwwlk  29984  clwlkclwwlkf1lem2  29987  clwlkclwwlkf  29990  clwwisshclwws  29997  clwwlknlbonbgr1  30021  clwwlknon0  30075  clwwlknonel  30077  clwwlknonex2e  30092  3pthdlem1  30146  eupth2  30221  nfrgr2v  30254  frgr3vlem1  30255  1to2vfriswmgr  30261  1to3vfriswmgr  30262  vdgn1frgrv2  30278  frgrncvvdeqlem9  30289  frgrwopreglem4a  30292  frgrregorufr0  30306  frgrregorufr  30307  2wspmdisj  30319  2clwwlk2clwwlklem  30328  frgrreggt1  30375  frgrreg  30376  frgrregord13  30378  aevdemo  30442  shsvs  31305  0cnop  31961  0cnfn  31962  cnlnssadj  32062  ssmd1  32293  ssmd2  32294  atexch  32363  mdsymlem4  32388  sumdmdlem  32400  ifeqeqx  32524  fmptcof2  32641  padct  32705  nnindf  32807  drng0mxidl  33448  constr01  33776  pwsiga  34164  pwldsys  34191  ldsysgenld  34194  fiunelros  34208  breprexp  34667  bnj151  34910  bnj594  34945  bnj600  34952  trssfir1om  35143  trssfir1omregs  35153  subfacp1lem6  35250  erdszelem8  35263  cvmliftlem7  35356  cvmliftlem10  35359  cvmlift2lem12  35379  sat1el2xp  35444  mrsubfval  35573  msubfval  35589  mclsssvlem  35627  antnestlaw2  35757  funpartfv  36010  endofsegid  36150  broutsideof2  36187  a1i24  36366  nn0prpwlem  36387  nn0prpw  36388  ordcmp  36512  findreccl  36518  bj-ax6e  36733  bj-ax12v3ALT  36751  bj-xpnzex  37024  bj-ideqg1  37229  rdgssun  37443  finxp00  37467  domalom  37469  isinf2  37470  fvineqsneq  37477  wl-spae  37586  wl-nfs1t  37602  poimirlem27  37707  ovoliunnfl  37722  voliunnfl  37724  volsupnfl  37725  itg2addnclem3  37733  itg2addnc  37734  ftc1anc  37761  areacirclem1  37768  sdclem2  37802  fdc  37805  mettrifi  37817  isexid2  37915  zerdivemp1x  38007  smprngopr  38112  mpobi123f  38222  mptbi12f  38226  ac6s6  38232  relcnveq3  38379  mopickr  38415  elrelscnveq3  38659  disjlem14  38916  jca3  38975  ax12fromc15  39024  hbequid  39028  dvelimf-o  39048  ax12eq  39060  ax12el  39061  ax12indalem  39064  ax12inda2ALT  39065  ax12inda2  39066  lfl1dim  39240  lfl1dim2N  39241  lkreqN  39289  cvrexchlem  39538  ps-2  39597  paddasslem14  39952  idldil  40233  isltrn2N  40239  cdleme25a  40472  dibglbN  41285  dihlsscpre  41353  dvh4dimlem  41562  lcfl7N  41620  mapdval2N  41749  dvrelog2b  42179  aks6d1c6lem3  42285  monotoddzzfi  43059  onov0suclim  43391  onmcl  43448  omabs2  43449  tfsconcat0b  43463  naddgeoa  43511  rp-fakeimass  43629  clublem  43727  grur1cld  44349  ee121  44622  ee122  44623  rspsbc2  44651  ax6e2ndeq  44676  vd12  44717  vd13  44718  ee221  44767  ee212  44769  ee112  44772  ee211  44775  ee210  44777  ee201  44779  ee120  44781  ee021  44783  ee012  44785  ee102  44787  ee03  44857  ee31  44868  ee31an  44870  ee123  44879  ax6e2ndeqVD  45025  ax6e2ndeqALT  45047  refsum2cnlem1  45158  fiiuncl  45186  eliin2f  45225  disjrnmpt2  45309  disjinfi  45313  rnmptbdlem  45376  allbutfi  45515  infxrunb3rnmpt  45550  infrpgernmpt  45587  monoordxrv  45603  mccl  45722  constlimc  45748  limclner  45773  xlimmnfvlem1  45954  xlimpnfvlem1  45958  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  dvnprodlem3  46070  stoweidlem31  46153  pwsal  46437  prsal  46440  sge0pnffigt  46518  sge0ltfirp  46522  0ome  46651  hoicvrrex  46678  hoidmvle  46722  ovnhoilem1  46723  ovnlecvr2  46732  smflimlem3  46895  ormkglobd  46997  chnsubseqword  47000  funressnfv  47167  euoreqb  47233  ndmaovass  47330  afv2orxorb  47352  otiunsndisjX  47403  nltle2tri  47437  m1modmmod  47482  smonoord  47495  iccpartigtl  47547  icceuelpartlem  47559  iccpartnel  47562  sprsymrelfolem2  47617  prproropf1olem4  47630  paireqne  47635  reupr  47646  reuopreuprim  47650  fmtnoprmfac1  47689  fmtnoprmfac2  47691  prmdvdsfmtnof1lem2  47709  31prm  47721  lighneallem3  47731  lighneallem4b  47733  lighneallem4  47734  lighneal  47735  nn0o1gt2ALTV  47818  nn0oALTV  47820  odd2prm2  47842  even3prm2  47843  fpprwppr  47863  stgoldbwt  47900  sbgoldbwt  47901  sbgoldbalt  47905  sbgoldbo  47911  nnsum3primesgbe  47916  wtgoldbnnsum4prm  47926  bgoldbnnsum3prm  47928  bgoldbtbndlem2  47930  bgoldbtbndlem3  47931  bgoldbtbndlem4  47932  bgoldbtbnd  47933  bgoldbachlt  47937  tgblthelfgott  47939  dfclnbgr6  47980  grimco  48013  uhgrimisgrgric  48055  grtriprop  48065  usgrgrtrirex  48074  isubgr3stgrlem6  48095  isubgr3stgrlem8  48097  grlimprclnbgr  48120  grlimgrtri  48127  gpgedg2ov  48190  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem2  48196  gpg5nbgrvtx13starlem3  48197  gpgcubic  48203  gpg5nbgr3star  48205  gpgprismgr4cycllem7  48225  pgnbgreunbgrlem2  48241  gpg5edgnedg  48254  upgrwlkupwlk  48264  rngccatidALTV  48396  ringccatidALTV  48430  lincdifsn  48549  lindslinindimp2lem1  48583  lindsrng01  48593  ldepsnlinc  48633  blen1b  48713  nn0sumshdiglemB  48745  nn0sumshdiglem1  48746  reorelicc  48835  rrx2xpref1o  48843  rrx2plord2  48847  rrxlinesc  48860  line2ylem  48876  line2xlem  48878  thincmon  49558  thincepi  49559