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  1627  meredith  1641  stdpc4  2069  ax12  2421  ax12vALT  2467  nfsb4t  2497  moexexlem  2619  pm2.61da3ne  3014  ralrimivw  3125  rexlimdvw  3135  reximdv  3144  vtocl2d  3519  reuind  3715  reuan  3850  2reu4  4476  rabeqsnd  4623  tppreqb  4759  ssprsseq  4779  n0snor2el  4787  prnebg  4810  prel12g  4818  elpreqprlem  4820  3elpr2eq  4860  disjord  5084  disjiund  5086  dtruALT2  5312  exneq  5382  dtruOLD  5388  propssopi  5455  opthhausdorff  5464  fr0  5601  ssrel2  5732  poltletr  6085  reuop  6245  ordsssuc2  6404  ordnbtwn  6406  ndmfv  6859  fveqres  6871  fmptco  7067  funsndifnop  7089  tpres  7141  fntpb  7149  elunirn  7191  isof1oopb  7266  ndmovord  7543  ordsucelsuc  7761  tfinds  7800  tfindsg  7801  limomss  7811  findsg  7837  finds1  7839  xpexr  7858  resf1extb  7874  bropopvvv  8030  bropfvvvvlem  8031  bropfvvvv  8032  soxp  8069  poseq  8098  suppun  8124  extmptsuppeq  8128  funsssuppss  8130  suppss  8134  suppss2  8140  suppssfv  8142  suppco  8146  mpoxopynvov0  8158  smofvon2  8286  oaordi  8471  oawordeulem  8479  odi  8504  omeulem1  8507  brdomg  8891  snmapen  8970  fopwdom  9009  fodomr  9052  mapxpen  9067  infensuc  9079  fineqvlem  9167  fineqv  9168  xpfiOLD  9228  fodomfir  9237  finsschain  9268  fsuppun  9296  fsuppunbi  9298  funsnfsupp  9301  dffi3  9340  fisup2g  9378  fisupcl  9379  fiinf2g  9411  infsupprpr  9415  wemapso2  9464  epnsym  9524  en3lplem2  9528  preleqg  9530  inf3lemd  9542  r1ordg  9693  r1val1  9701  r1pw  9760  r1pwALT  9761  rankxplim3  9796  eldju2ndl  9839  eldju2ndr  9840  carddomi2  9885  fidomtri  9908  alephon  9982  alephcard  9983  alephnbtwn  9984  alephordi  9987  iunfictbso  10027  fin23lem30  10255  fin1a2lem10  10322  axdc3lem2  10364  axdc3lem4  10366  alephval2  10485  cfpwsdom  10497  axextnd  10504  axrepnd  10507  axpownd  10514  axregnd  10517  axinfndlem1  10518  fpwwe2lem11  10554  wunfi  10634  addnidpi  10814  pinq  10840  mulgt0sr  11018  dedekind  11297  nnind  12164  nn1m1nn  12167  nn0n0n1ge2b  12471  nn0lt2  12557  nn0le2is012  12558  uzm1  12791  uzinfi  12847  nn01to3  12860  xrltnsym  13057  xrlttri  13059  xrlttr  13060  qbtwnxr  13120  xltnegi  13136  xnn0xaddcl  13155  xlt2add  13180  xrsupsslem  13227  xrinfmsslem  13228  xrub  13232  reltxrnmnf  13263  fzdif1  13526  fzospliti  13612  elfzonlteqm1  13662  fzoopth  13683  elfznelfzo  13693  injresinjlem  13708  injresinj  13709  modfzo0difsn  13868  addmodlteq  13871  ssnn0fi  13910  fsuppmapnn0fiub0  13918  suppssfz  13919  seqfveq2  13949  monoord  13957  seqf1o  13968  seqhomo  13974  expnngt1  14166  faclbnd4lem4  14221  hasheqf1oi  14276  hashrabsn1  14299  hashgt0elex  14326  hash1snb  14344  hashf1lem2  14381  hashf1  14382  seqcoll  14389  hashle2pr  14402  pr2pwpr  14404  hashge2el2difr  14406  swrdnnn0nd  14581  swrdnd0  14582  pfxnd0  14613  swrdswrd  14629  pfxccatin12lem3  14656  pfxccat3  14658  swrdccat3blem  14663  repsdf2  14702  repswsymballbi  14704  cshw0  14718  cshwmodn  14719  cshwn  14721  cshwcl  14722  cshwlen  14723  cshw1  14746  2cshwcshw  14750  cshimadifsn  14754  s3sndisj  14892  s3iunsndisj  14893  relexprelg  14963  relexpnndm  14966  relexpaddg  14978  relexpaddd  14979  rtrclreclem4  14986  relexpindlem  14988  rexuz3  15274  rexanuz2  15275  limsupgre  15406  rlimconst  15469  caurcvg  15602  caucvg  15604  sumss  15649  fsumcl2lem  15656  modfsummods  15718  fsumrlim  15736  fsumo1  15737  fprodcl2lem  15875  dvdsaddre2b  16236  dvdsabseq  16242  mod2eq1n2dvds  16276  nno  16311  sumeven  16316  sumodd  16317  nn0rppwr  16490  nn0seqcvgd  16499  lcmdvds  16537  lcmfunsnlem2  16569  lcmfunsnlem  16570  divgcdcoprm0  16594  ge2nprmge4  16630  exprmfct  16633  rpexp1i  16652  prm23lt5  16744  prm23ge5  16745  pcz  16811  pcadd  16819  pcmptcl  16821  oddprmdvds  16833  prmgaplem6  16986  prmgaplem7  16987  cshwshashlem1  17025  cshwsdisj  17028  prmlem0  17035  setsstruct  17105  ressress  17176  initoeu2lem2  17940  mgm2nsgrplem2  18811  mgm2nsgrplem3  18812  dfgrp2e  18860  dfgrp3e  18937  cyccom  19100  symgextf1  19318  gsmsymgrfix  19325  gsmsymgreq  19329  sylow1lem1  19495  efgsf  19626  efgrelexlema  19646  dprdss  19928  ablfac1eulem  19971  01eq0ringOLD  20434  nrhmzr  20440  funcrngcsetcALT  20544  lssssr  20875  psgnodpm  21513  psrvscafval  21873  mplcoe1  21960  mplcoe5  21963  mpfrcl  22008  mamudm  22298  matmulcell  22348  dmatmul  22400  scmatsgrp1  22425  mavmuldm  22453  mavmulsolcl  22454  mdetunilem9  22523  cramerlem3  22592  cramer0  22593  chpscmatgsumbin  22747  chp0mat  22749  fvmptnn04ifc  22755  fvmptnn04ifd  22756  epttop  22912  neiptopnei  23035  fiuncmp  23307  1stcrest  23356  kgenss  23446  hmeofval  23661  fbun  23743  fgss2  23777  filuni  23788  filssufilg  23814  filufint  23823  hausflimi  23883  hausflim  23884  hauspwpwf1  23890  fclscmp  23933  alexsubALTlem4  23953  ptcmplem3  23957  ptcmplem5  23959  cstucnd  24187  isxmet2d  24231  imasdsf1olem  24277  blfps  24310  blf  24311  metrest  24428  nrginvrcn  24596  nmoge0  24625  nmoleub  24635  fsumcn  24777  cmetcaulem  25204  iscmet3  25209  iscmet2  25210  bcthlem2  25241  ovolicc2lem3  25436  itg2seq  25659  itg2splitlem  25665  itgeq1fOLD  25689  itgeq2  25695  iblcnlem  25706  itgfsum  25744  limcnlp  25795  perfdvf  25820  dvnres  25849  dvmptfsum  25895  c1lip1  25918  dvply2g  26208  taylply2  26291  abelth  26367  cxpsqrtth  26655  rlimcnp  26891  xrlimcnp  26894  jensen  26915  ppiublem1  27129  dchrelbas3  27165  bcmono  27204  zabsle1  27223  gausslemma2dlem0f  27288  gausslemma2dlem1a  27292  gausslemma2dlem4  27296  lgsquad2lem2  27312  2lgslem1a1  27316  2lgslem3  27331  2lgs  27334  2lgsoddprm  27343  2sqlem10  27355  2sqnn  27366  addsqnreup  27370  2sqreultblem  27375  2sqreunnltblem  27378  pntrsumbnd2  27494  pntpbnd1  27513  pntlem3  27536  nolesgn2o  27599  noetalem1  27669  bday0b  27762  leftf  27797  rightf  27798  oldss  27810  addscutlem  27907  negscut  27968  mulscutlem  28057  n0s0suc  28257  n0sfincut  28269  n0s0m1  28275  nn1m1nns  28286  axcontlem7  28933  elntg2  28948  ausgrusgrb  29128  usgredg2v  29190  lfuhgr1v0e  29217  subumgredg2  29248  upgrreslem  29267  umgrreslem  29268  fusgrfisbase  29291  nbuhgr  29306  uhgrnbgr0nb  29317  nbgr0edglem  29319  nbgr1vtx  29321  cusgredg  29387  cusgrsizeinds  29416  sizusglecusg  29427  finsumvtxdg2size  29514  ewlkle  29569  upgriswlk  29604  pthdivtx  29690  dfpth2  29692  usgr2trlncl  29723  crctcshwlkn0lem4  29776  wwlksn  29800  iswwlksnon  29816  iswspthsnon  29819  wwlksm1edg  29844  wwlksnfi  29869  2pthdlem1  29893  umgr2wlk  29912  umgrclwwlkge2  29953  clwlkclwwlklem2a  29960  clwlkclwwlk  29964  clwlkclwwlkf1lem2  29967  clwlkclwwlkf  29970  clwwisshclwws  29977  clwwlknlbonbgr1  30001  clwwlknon0  30055  clwwlknonel  30057  clwwlknonex2e  30072  3pthdlem1  30126  eupth2  30201  nfrgr2v  30234  frgr3vlem1  30235  1to2vfriswmgr  30241  1to3vfriswmgr  30242  vdgn1frgrv2  30258  frgrncvvdeqlem9  30269  frgrwopreglem4a  30272  frgrregorufr0  30286  frgrregorufr  30287  2wspmdisj  30299  2clwwlk2clwwlklem  30308  frgrreggt1  30355  frgrreg  30356  frgrregord13  30358  aevdemo  30422  shsvs  31285  0cnop  31941  0cnfn  31942  cnlnssadj  32042  ssmd1  32273  ssmd2  32274  atexch  32343  mdsymlem4  32368  sumdmdlem  32380  ifeqeqx  32504  fmptcof2  32614  padct  32676  nnindf  32777  drng0mxidl  33423  constr01  33708  pwsiga  34096  pwldsys  34123  ldsysgenld  34126  fiunelros  34140  breprexp  34600  bnj151  34843  bnj594  34878  bnj600  34885  subfacp1lem6  35157  erdszelem8  35170  cvmliftlem7  35263  cvmliftlem10  35266  cvmlift2lem12  35286  sat1el2xp  35351  mrsubfval  35480  msubfval  35496  mclsssvlem  35534  antnestlaw2  35664  funpartfv  35918  endofsegid  36058  broutsideof2  36095  a1i24  36274  nn0prpwlem  36295  nn0prpw  36296  ordcmp  36420  findreccl  36426  bj-ax6e  36641  bj-ax12v3ALT  36659  bj-xpnzex  36932  bj-ideqg1  37137  rdgssun  37351  finxp00  37375  domalom  37377  isinf2  37378  fvineqsneq  37385  wl-spae  37494  wl-nfs1t  37510  poimirlem27  37626  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  itg2addnclem3  37652  itg2addnc  37653  ftc1anc  37680  areacirclem1  37687  sdclem2  37721  fdc  37724  mettrifi  37736  isexid2  37834  zerdivemp1x  37926  smprngopr  38031  mpobi123f  38141  mptbi12f  38145  ac6s6  38151  relcnveq3  38294  mopickr  38330  elrelscnveq3  38467  disjlem14  38775  jca3  38834  ax12fromc15  38883  hbequid  38887  dvelimf-o  38907  ax12eq  38919  ax12el  38920  ax12indalem  38923  ax12inda2ALT  38924  ax12inda2  38925  lfl1dim  39099  lfl1dim2N  39100  lkreqN  39148  cvrexchlem  39398  ps-2  39457  paddasslem14  39812  idldil  40093  isltrn2N  40099  cdleme25a  40332  dibglbN  41145  dihlsscpre  41213  dvh4dimlem  41422  lcfl7N  41480  mapdval2N  41609  dvrelog2b  42039  aks6d1c6lem3  42145  monotoddzzfi  42915  onov0suclim  43247  onmcl  43304  omabs2  43305  tfsconcat0b  43319  naddgeoa  43367  rp-fakeimass  43485  clublem  43583  grur1cld  44205  ee121  44479  ee122  44480  rspsbc2  44508  ax6e2ndeq  44533  vd12  44574  vd13  44575  ee221  44624  ee212  44626  ee112  44629  ee211  44632  ee210  44634  ee201  44636  ee120  44638  ee021  44640  ee012  44642  ee102  44644  ee03  44714  ee31  44725  ee31an  44727  ee123  44736  ax6e2ndeqVD  44882  ax6e2ndeqALT  44904  refsum2cnlem1  45015  fiiuncl  45043  eliin2f  45082  disjrnmpt2  45166  disjinfi  45170  rnmptbdlem  45233  allbutfi  45373  infxrunb3rnmpt  45408  infrpgernmpt  45445  monoordxrv  45461  mccl  45580  constlimc  45606  limclner  45633  xlimmnfvlem1  45814  xlimpnfvlem1  45818  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvnprodlem3  45930  stoweidlem31  46013  pwsal  46297  prsal  46300  sge0pnffigt  46378  sge0ltfirp  46382  0ome  46511  hoicvrrex  46538  hoidmvle  46582  ovnhoilem1  46583  ovnlecvr2  46592  smflimlem3  46755  ormkglobd  46857  funressnfv  47028  euoreqb  47094  ndmaovass  47191  afv2orxorb  47213  otiunsndisjX  47264  nltle2tri  47298  m1modmmod  47343  smonoord  47356  iccpartigtl  47408  icceuelpartlem  47420  iccpartnel  47423  sprsymrelfolem2  47478  prproropf1olem4  47491  paireqne  47496  reupr  47507  reuopreuprim  47511  fmtnoprmfac1  47550  fmtnoprmfac2  47552  prmdvdsfmtnof1lem2  47570  31prm  47582  lighneallem3  47592  lighneallem4b  47594  lighneallem4  47595  lighneal  47596  nn0o1gt2ALTV  47679  nn0oALTV  47681  odd2prm2  47703  even3prm2  47704  fpprwppr  47724  stgoldbwt  47761  sbgoldbwt  47762  sbgoldbalt  47766  sbgoldbo  47772  nnsum3primesgbe  47777  wtgoldbnnsum4prm  47787  bgoldbnnsum3prm  47789  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  bgoldbtbndlem4  47793  bgoldbtbnd  47794  bgoldbachlt  47798  tgblthelfgott  47800  dfclnbgr6  47841  grimco  47874  uhgrimisgrgric  47916  grtriprop  47926  usgrgrtrirex  47935  isubgr3stgrlem6  47956  isubgr3stgrlem8  47958  grlimprclnbgr  47981  grlimgrtri  47988  gpgedg2ov  48051  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem2  48057  gpg5nbgrvtx13starlem3  48058  gpgcubic  48064  gpg5nbgr3star  48066  gpgprismgr4cycllem7  48086  pgnbgreunbgrlem2  48102  gpg5edgnedg  48115  upgrwlkupwlk  48125  rngccatidALTV  48257  ringccatidALTV  48291  lincdifsn  48410  lindslinindimp2lem1  48444  lindsrng01  48454  ldepsnlinc  48494  blen1b  48574  nn0sumshdiglemB  48606  nn0sumshdiglem1  48607  reorelicc  48696  rrx2xpref1o  48704  rrx2plord2  48708  rrxlinesc  48721  line2ylem  48737  line2xlem  48739  thincmon  49419  thincepi  49420