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  629  anbi1d  630  pm3.4  809  impsingle  1625  meredith  1639  stdpc4  2068  ax12  2431  ax12vALT  2477  nfsb4t  2507  moexexlem  2629  pm2.61da3ne  3037  ralrimivw  3156  rexlimdvw  3166  reximdv  3176  vtocl2d  3574  reuind  3775  reuan  3918  2reu4  4546  rabeqsnd  4691  tppreqb  4830  ssprsseq  4850  n0snor2el  4858  prnebg  4880  prel12g  4888  elpreqprlem  4890  3elpr2eq  4930  disjord  5155  disjiund  5157  dtruALT2  5388  exneq  5455  dtruOLD  5461  propssopi  5527  opthhausdorff  5536  fr0  5678  ssrel2  5809  poltletr  6164  reuop  6324  ordsssuc2  6486  ordnbtwn  6488  ndmfv  6955  fveqres  6967  fmptco  7163  funsndifnop  7185  tpres  7238  fntpb  7246  elunirn  7288  isof1oopb  7361  fvmptopabOLD  7505  ndmovord  7640  ordsucelsuc  7858  tfinds  7897  tfindsg  7898  limomss  7908  findsg  7937  finds1  7939  xpexr  7958  bropopvvv  8131  bropfvvvvlem  8132  bropfvvvv  8133  soxp  8170  poseq  8199  suppun  8225  extmptsuppeq  8229  funsssuppss  8231  suppss  8235  suppss2  8241  suppssfv  8243  suppco  8247  mpoxopynvov0  8259  smofvon2  8412  oaordi  8602  oawordeulem  8610  odi  8635  omeulem1  8638  brdomg  9016  brdomgOLD  9017  snmapen  9103  fopwdom  9146  fodomr  9194  mapxpen  9209  infensuc  9221  onomeneqOLD  9292  fineqvlem  9325  fineqv  9326  xpfiOLD  9387  fodomfir  9396  finsschain  9429  fsuppun  9456  fsuppunbi  9458  funsnfsupp  9461  dffi3  9500  fisup2g  9537  fisupcl  9538  fiinf2g  9569  infsupprpr  9573  wemapso2  9622  epnsym  9678  en3lplem2  9682  preleqg  9684  inf3lemd  9696  r1ordg  9847  r1val1  9855  r1pw  9914  r1pwALT  9915  rankxplim3  9950  eldju2ndl  9993  eldju2ndr  9994  carddomi2  10039  fidomtri  10062  pr2neOLD  10074  alephon  10138  alephcard  10139  alephnbtwn  10140  alephordi  10143  iunfictbso  10183  fin23lem30  10411  fin1a2lem10  10478  axdc3lem2  10520  axdc3lem4  10522  alephval2  10641  cfpwsdom  10653  axextnd  10660  axrepnd  10663  axpownd  10670  axregnd  10673  axinfndlem1  10674  fpwwe2lem11  10710  wunfi  10790  addnidpi  10970  pinq  10996  mulgt0sr  11174  dedekind  11453  nnind  12311  nn1m1nn  12314  nn0n0n1ge2b  12621  nn0lt2  12706  nn0le2is012  12707  uzm1  12941  uzinfi  12993  nn01to3  13006  xrltnsym  13199  xrlttri  13201  xrlttr  13202  qbtwnxr  13262  xltnegi  13278  xnn0xaddcl  13297  xlt2add  13322  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  reltxrnmnf  13404  fzospliti  13748  elfzonlteqm1  13792  fzoopth  13812  elfznelfzo  13822  injresinjlem  13837  injresinj  13838  modfzo0difsn  13994  addmodlteq  13997  ssnn0fi  14036  fsuppmapnn0fiub0  14044  suppssfz  14045  seqfveq2  14075  monoord  14083  seqf1o  14094  seqhomo  14100  expnngt1  14290  faclbnd4lem4  14345  hasheqf1oi  14400  hashrabsn1  14423  hashgt0elex  14450  hash1snb  14468  hashf1lem2  14505  hashf1  14506  seqcoll  14513  hashle2pr  14526  pr2pwpr  14528  hashge2el2difr  14530  swrdnnn0nd  14704  swrdnd0  14705  pfxnd0  14736  swrdswrd  14753  pfxccatin12lem3  14780  pfxccat3  14782  swrdccat3blem  14787  repsdf2  14826  repswsymballbi  14828  cshw0  14842  cshwmodn  14843  cshwn  14845  cshwcl  14846  cshwlen  14847  cshw1  14870  2cshwcshw  14874  cshimadifsn  14878  s3sndisj  15016  s3iunsndisj  15017  relexprelg  15087  relexpnndm  15090  relexpaddg  15102  relexpaddd  15103  rtrclreclem4  15110  relexpindlem  15112  rexuz3  15397  rexanuz2  15398  limsupgre  15527  rlimconst  15590  caurcvg  15725  caucvg  15727  sumss  15772  fsumcl2lem  15779  modfsummods  15841  fsumrlim  15859  fsumo1  15860  fprodcl2lem  15998  dvdsaddre2b  16355  dvdsabseq  16361  mod2eq1n2dvds  16395  nno  16430  sumeven  16435  sumodd  16436  nn0rppwr  16608  nn0seqcvgd  16617  lcmdvds  16655  lcmfunsnlem2  16687  lcmfunsnlem  16688  divgcdcoprm0  16712  ge2nprmge4  16748  exprmfct  16751  rpexp1i  16770  prm23lt5  16861  prm23ge5  16862  pcz  16928  pcadd  16936  pcmptcl  16938  oddprmdvds  16950  prmgaplem6  17103  prmgaplem7  17104  cshwshashlem1  17143  cshwsdisj  17146  prmlem0  17153  setsstruct  17223  ressress  17307  initoeu2lem2  18082  mgm2nsgrplem2  18954  mgm2nsgrplem3  18955  dfgrp2e  19003  dfgrp3e  19080  cyccom  19243  symgextf1  19463  gsmsymgrfix  19470  gsmsymgreq  19474  sylow1lem1  19640  efgsf  19771  efgrelexlema  19791  dprdss  20073  ablfac1eulem  20116  01eq0ringOLD  20557  nrhmzr  20563  funcrngcsetcALT  20663  lssssr  20975  psgnodpm  21629  psrvscafval  21991  mplcoe1  22078  mplcoe5  22081  mpfrcl  22132  mamudm  22420  matmulcell  22472  dmatmul  22524  scmatsgrp1  22549  mavmuldm  22577  mavmulsolcl  22578  mdetunilem9  22647  cramerlem3  22716  cramer0  22717  chpscmatgsumbin  22871  chp0mat  22873  fvmptnn04ifc  22879  fvmptnn04ifd  22880  epttop  23037  neiptopnei  23161  fiuncmp  23433  1stcrest  23482  kgenss  23572  hmeofval  23787  fbun  23869  fgss2  23903  filuni  23914  filssufilg  23940  filufint  23949  hausflimi  24009  hausflim  24010  hauspwpwf1  24016  fclscmp  24059  alexsubALTlem4  24079  ptcmplem3  24083  ptcmplem5  24085  cstucnd  24314  isxmet2d  24358  imasdsf1olem  24404  blfps  24437  blf  24438  metrest  24558  nrginvrcn  24734  nmoge0  24763  nmoleub  24773  fsumcn  24913  cmetcaulem  25341  iscmet3  25346  iscmet2  25347  bcthlem2  25378  ovolicc2lem3  25573  itg2seq  25797  itg2splitlem  25803  itgeq1fOLD  25827  itgeq2  25833  iblcnlem  25844  itgfsum  25882  limcnlp  25933  perfdvf  25958  dvnres  25987  dvmptfsum  26033  c1lip1  26056  dvply2g  26344  taylply2  26427  abelth  26503  cxpsqrtth  26790  rlimcnp  27026  xrlimcnp  27029  jensen  27050  ppiublem1  27264  dchrelbas3  27300  bcmono  27339  zabsle1  27358  gausslemma2dlem0f  27423  gausslemma2dlem1a  27427  gausslemma2dlem4  27431  lgsquad2lem2  27447  2lgslem1a1  27451  2lgslem3  27466  2lgs  27469  2lgsoddprm  27478  2sqlem10  27490  2sqnn  27501  addsqnreup  27505  2sqreultblem  27510  2sqreunnltblem  27513  pntrsumbnd2  27629  pntpbnd1  27648  pntlem3  27671  nolesgn2o  27734  noetalem1  27804  bday0b  27893  leftf  27922  rightf  27923  addscutlem  28028  negscut  28089  mulscutlem  28175  n0s0suc  28363  n0s0m1  28377  axcontlem7  29003  elntg2  29018  ausgrusgrb  29200  usgredg2v  29262  lfuhgr1v0e  29289  subumgredg2  29320  upgrreslem  29339  umgrreslem  29340  fusgrfisbase  29363  nbuhgr  29378  uhgrnbgr0nb  29389  nbgr0edglem  29391  nbgr1vtx  29393  cusgredg  29459  cusgrsizeinds  29488  sizusglecusg  29499  finsumvtxdg2size  29586  ewlkle  29641  upgriswlk  29677  pthdivtx  29765  usgr2trlncl  29796  crctcshwlkn0lem4  29846  wwlksn  29870  iswwlksnon  29886  iswspthsnon  29889  wwlksm1edg  29914  wwlksnfi  29939  2pthdlem1  29963  umgr2wlk  29982  umgrclwwlkge2  30023  clwlkclwwlklem2a  30030  clwlkclwwlk  30034  clwlkclwwlkf1lem2  30037  clwlkclwwlkf  30040  clwwisshclwws  30047  clwwlknlbonbgr1  30071  clwwlknon0  30125  clwwlknonel  30127  clwwlknonex2e  30142  3pthdlem1  30196  eupth2  30271  nfrgr2v  30304  frgr3vlem1  30305  1to2vfriswmgr  30311  1to3vfriswmgr  30312  vdgn1frgrv2  30328  frgrncvvdeqlem9  30339  frgrwopreglem4a  30342  frgrregorufr0  30356  frgrregorufr  30357  2wspmdisj  30369  2clwwlk2clwwlklem  30378  frgrreggt1  30425  frgrreg  30426  frgrregord13  30428  aevdemo  30492  shsvs  31355  0cnop  32011  0cnfn  32012  cnlnssadj  32112  ssmd1  32343  ssmd2  32344  atexch  32413  mdsymlem4  32438  sumdmdlem  32450  ifeqeqx  32565  fmptcof2  32675  padct  32733  nnindf  32823  drng0mxidl  33469  constr01  33732  pwsiga  34094  pwldsys  34121  ldsysgenld  34124  fiunelros  34138  breprexp  34610  bnj151  34853  bnj594  34888  bnj600  34895  subfacp1lem6  35153  erdszelem8  35166  cvmliftlem7  35259  cvmliftlem10  35262  cvmlift2lem12  35282  sat1el2xp  35347  mrsubfval  35476  msubfval  35492  mclsssvlem  35530  funpartfv  35909  endofsegid  36049  broutsideof2  36086  a1i24  36267  nn0prpwlem  36288  nn0prpw  36289  ordcmp  36413  findreccl  36419  bj-ax6e  36634  bj-ax12v3ALT  36652  bj-xpnzex  36925  bj-ideqg1  37130  rdgssun  37344  finxp00  37368  domalom  37370  isinf2  37371  fvineqsneq  37378  wl-spae  37475  wl-nfs1t  37491  poimirlem27  37607  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  itg2addnclem3  37633  itg2addnc  37634  ftc1anc  37661  areacirclem1  37668  sdclem2  37702  fdc  37705  mettrifi  37717  isexid2  37815  zerdivemp1x  37907  smprngopr  38012  mpobi123f  38122  mptbi12f  38126  ac6s6  38132  relcnveq3  38277  mopickr  38319  elrelscnveq3  38447  disjlem14  38754  jca3  38812  ax12fromc15  38861  hbequid  38865  dvelimf-o  38885  ax12eq  38897  ax12el  38898  ax12indalem  38901  ax12inda2ALT  38902  ax12inda2  38903  lfl1dim  39077  lfl1dim2N  39078  lkreqN  39126  cvrexchlem  39376  ps-2  39435  paddasslem14  39790  idldil  40071  isltrn2N  40077  cdleme25a  40310  dibglbN  41123  dihlsscpre  41191  dvh4dimlem  41400  lcfl7N  41458  mapdval2N  41587  dvrelog2b  42023  aks6d1c6lem3  42129  monotoddzzfi  42899  onov0suclim  43236  onmcl  43293  omabs2  43294  tfsconcat0b  43308  naddgeoa  43356  rp-fakeimass  43474  clublem  43572  grur1cld  44201  ee121  44476  ee122  44477  rspsbc2  44505  ax6e2ndeq  44530  vd12  44571  vd13  44572  ee221  44621  ee212  44623  ee112  44626  ee211  44629  ee210  44631  ee201  44633  ee120  44635  ee021  44637  ee012  44639  ee102  44641  ee03  44712  ee31  44723  ee31an  44725  ee123  44734  ax6e2ndeqVD  44880  ax6e2ndeqALT  44902  refsum2cnlem1  44937  fiiuncl  44967  eliin2f  45006  disjrnmpt2  45095  disjinfi  45099  rnmptbdlem  45164  allbutfi  45308  infxrunb3rnmpt  45343  infrpgernmpt  45380  monoordxrv  45397  mccl  45519  constlimc  45545  limclner  45572  xlimmnfvlem1  45753  xlimpnfvlem1  45757  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvmptfprod  45866  dvnprodlem3  45869  stoweidlem31  45952  pwsal  46236  prsal  46239  sge0pnffigt  46317  sge0ltfirp  46321  0ome  46450  hoicvrrex  46477  hoidmvle  46521  ovnhoilem1  46522  ovnlecvr2  46531  smflimlem3  46694  funressnfv  46958  euoreqb  47024  ndmaovass  47121  afv2orxorb  47143  otiunsndisjX  47194  nltle2tri  47228  smonoord  47245  iccpartigtl  47297  icceuelpartlem  47309  iccpartnel  47312  sprsymrelfolem2  47367  prproropf1olem4  47380  paireqne  47385  reupr  47396  reuopreuprim  47400  fmtnoprmfac1  47439  fmtnoprmfac2  47441  prmdvdsfmtnof1lem2  47459  31prm  47471  lighneallem3  47481  lighneallem4b  47483  lighneallem4  47484  lighneal  47485  nn0o1gt2ALTV  47568  nn0oALTV  47570  odd2prm2  47592  even3prm2  47593  fpprwppr  47613  stgoldbwt  47650  sbgoldbwt  47651  sbgoldbalt  47655  sbgoldbo  47661  nnsum3primesgbe  47666  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  bgoldbachlt  47687  tgblthelfgott  47689  dfclnbgr6  47728  grimco  47764  uhgrimisgrgric  47783  grtriprop  47792  usgrgrtrirex  47799  grlimgrtri  47820  upgrwlkupwlk  47863  rngccatidALTV  47995  ringccatidALTV  48029  lincdifsn  48153  lindslinindimp2lem1  48187  lindsrng01  48197  ldepsnlinc  48237  m1modmmod  48255  blen1b  48322  nn0sumshdiglemB  48354  nn0sumshdiglem1  48355  reorelicc  48444  rrx2xpref1o  48452  rrx2plord2  48456  rrxlinesc  48469  line2ylem  48485  line2xlem  48487  thincmon  48701  thincepi  48702