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  1627  meredith  1641  stdpc4  2068  ax12  2428  ax12vALT  2474  nfsb4t  2504  moexexlem  2626  pm2.61da3ne  3031  ralrimivw  3150  rexlimdvw  3160  reximdv  3170  vtocl2d  3562  reuind  3759  reuan  3896  2reu4  4523  rabeqsnd  4669  tppreqb  4805  ssprsseq  4825  n0snor2el  4833  prnebg  4856  prel12g  4864  elpreqprlem  4866  3elpr2eq  4906  disjord  5132  disjiund  5134  dtruALT2  5370  exneq  5440  dtruOLD  5446  propssopi  5513  opthhausdorff  5522  fr0  5663  ssrel2  5795  poltletr  6152  reuop  6313  ordsssuc2  6475  ordnbtwn  6477  ndmfv  6941  fveqres  6953  fmptco  7149  funsndifnop  7171  tpres  7221  fntpb  7229  elunirn  7271  isof1oopb  7345  fvmptopabOLD  7488  ndmovord  7623  ordsucelsuc  7842  tfinds  7881  tfindsg  7882  limomss  7892  findsg  7919  finds1  7921  xpexr  7940  resf1extb  7956  bropopvvv  8115  bropfvvvvlem  8116  bropfvvvv  8117  soxp  8154  poseq  8183  suppun  8209  extmptsuppeq  8213  funsssuppss  8215  suppss  8219  suppss2  8225  suppssfv  8227  suppco  8231  mpoxopynvov0  8243  smofvon2  8396  oaordi  8584  oawordeulem  8592  odi  8617  omeulem1  8620  brdomg  8997  brdomgOLD  8998  snmapen  9078  fopwdom  9120  fodomr  9168  mapxpen  9183  infensuc  9195  onomeneqOLD  9266  fineqvlem  9298  fineqv  9299  xpfiOLD  9359  fodomfir  9368  finsschain  9399  fsuppun  9427  fsuppunbi  9429  funsnfsupp  9432  dffi3  9471  fisup2g  9508  fisupcl  9509  fiinf2g  9540  infsupprpr  9544  wemapso2  9593  epnsym  9649  en3lplem2  9653  preleqg  9655  inf3lemd  9667  r1ordg  9818  r1val1  9826  r1pw  9885  r1pwALT  9886  rankxplim3  9921  eldju2ndl  9964  eldju2ndr  9965  carddomi2  10010  fidomtri  10033  pr2neOLD  10045  alephon  10109  alephcard  10110  alephnbtwn  10111  alephordi  10114  iunfictbso  10154  fin23lem30  10382  fin1a2lem10  10449  axdc3lem2  10491  axdc3lem4  10493  alephval2  10612  cfpwsdom  10624  axextnd  10631  axrepnd  10634  axpownd  10641  axregnd  10644  axinfndlem1  10645  fpwwe2lem11  10681  wunfi  10761  addnidpi  10941  pinq  10967  mulgt0sr  11145  dedekind  11424  nnind  12284  nn1m1nn  12287  nn0n0n1ge2b  12595  nn0lt2  12681  nn0le2is012  12682  uzm1  12916  uzinfi  12970  nn01to3  12983  xrltnsym  13179  xrlttri  13181  xrlttr  13182  qbtwnxr  13242  xltnegi  13258  xnn0xaddcl  13277  xlt2add  13302  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  reltxrnmnf  13384  fzdif1  13645  fzospliti  13731  elfzonlteqm1  13780  fzoopth  13801  elfznelfzo  13811  injresinjlem  13826  injresinj  13827  modfzo0difsn  13984  addmodlteq  13987  ssnn0fi  14026  fsuppmapnn0fiub0  14034  suppssfz  14035  seqfveq2  14065  monoord  14073  seqf1o  14084  seqhomo  14090  expnngt1  14280  faclbnd4lem4  14335  hasheqf1oi  14390  hashrabsn1  14413  hashgt0elex  14440  hash1snb  14458  hashf1lem2  14495  hashf1  14496  seqcoll  14503  hashle2pr  14516  pr2pwpr  14518  hashge2el2difr  14520  swrdnnn0nd  14694  swrdnd0  14695  pfxnd0  14726  swrdswrd  14743  pfxccatin12lem3  14770  pfxccat3  14772  swrdccat3blem  14777  repsdf2  14816  repswsymballbi  14818  cshw0  14832  cshwmodn  14833  cshwn  14835  cshwcl  14836  cshwlen  14837  cshw1  14860  2cshwcshw  14864  cshimadifsn  14868  s3sndisj  15006  s3iunsndisj  15007  relexprelg  15077  relexpnndm  15080  relexpaddg  15092  relexpaddd  15093  rtrclreclem4  15100  relexpindlem  15102  rexuz3  15387  rexanuz2  15388  limsupgre  15517  rlimconst  15580  caurcvg  15713  caucvg  15715  sumss  15760  fsumcl2lem  15767  modfsummods  15829  fsumrlim  15847  fsumo1  15848  fprodcl2lem  15986  dvdsaddre2b  16344  dvdsabseq  16350  mod2eq1n2dvds  16384  nno  16419  sumeven  16424  sumodd  16425  nn0rppwr  16598  nn0seqcvgd  16607  lcmdvds  16645  lcmfunsnlem2  16677  lcmfunsnlem  16678  divgcdcoprm0  16702  ge2nprmge4  16738  exprmfct  16741  rpexp1i  16760  prm23lt5  16852  prm23ge5  16853  pcz  16919  pcadd  16927  pcmptcl  16929  oddprmdvds  16941  prmgaplem6  17094  prmgaplem7  17095  cshwshashlem1  17133  cshwsdisj  17136  prmlem0  17143  setsstruct  17213  ressress  17293  initoeu2lem2  18060  mgm2nsgrplem2  18932  mgm2nsgrplem3  18933  dfgrp2e  18981  dfgrp3e  19058  cyccom  19221  symgextf1  19439  gsmsymgrfix  19446  gsmsymgreq  19450  sylow1lem1  19616  efgsf  19747  efgrelexlema  19767  dprdss  20049  ablfac1eulem  20092  01eq0ringOLD  20531  nrhmzr  20537  funcrngcsetcALT  20641  lssssr  20952  psgnodpm  21606  psrvscafval  21968  mplcoe1  22055  mplcoe5  22058  mpfrcl  22109  mamudm  22399  matmulcell  22451  dmatmul  22503  scmatsgrp1  22528  mavmuldm  22556  mavmulsolcl  22557  mdetunilem9  22626  cramerlem3  22695  cramer0  22696  chpscmatgsumbin  22850  chp0mat  22852  fvmptnn04ifc  22858  fvmptnn04ifd  22859  epttop  23016  neiptopnei  23140  fiuncmp  23412  1stcrest  23461  kgenss  23551  hmeofval  23766  fbun  23848  fgss2  23882  filuni  23893  filssufilg  23919  filufint  23928  hausflimi  23988  hausflim  23989  hauspwpwf1  23995  fclscmp  24038  alexsubALTlem4  24058  ptcmplem3  24062  ptcmplem5  24064  cstucnd  24293  isxmet2d  24337  imasdsf1olem  24383  blfps  24416  blf  24417  metrest  24537  nrginvrcn  24713  nmoge0  24742  nmoleub  24752  fsumcn  24894  cmetcaulem  25322  iscmet3  25327  iscmet2  25328  bcthlem2  25359  ovolicc2lem3  25554  itg2seq  25777  itg2splitlem  25783  itgeq1fOLD  25807  itgeq2  25813  iblcnlem  25824  itgfsum  25862  limcnlp  25913  perfdvf  25938  dvnres  25967  dvmptfsum  26013  c1lip1  26036  dvply2g  26326  taylply2  26409  abelth  26485  cxpsqrtth  26772  rlimcnp  27008  xrlimcnp  27011  jensen  27032  ppiublem1  27246  dchrelbas3  27282  bcmono  27321  zabsle1  27340  gausslemma2dlem0f  27405  gausslemma2dlem1a  27409  gausslemma2dlem4  27413  lgsquad2lem2  27429  2lgslem1a1  27433  2lgslem3  27448  2lgs  27451  2lgsoddprm  27460  2sqlem10  27472  2sqnn  27483  addsqnreup  27487  2sqreultblem  27492  2sqreunnltblem  27495  pntrsumbnd2  27611  pntpbnd1  27630  pntlem3  27653  nolesgn2o  27716  noetalem1  27786  bday0b  27875  leftf  27904  rightf  27905  addscutlem  28010  negscut  28071  mulscutlem  28157  n0s0suc  28345  n0s0m1  28359  axcontlem7  28985  elntg2  29000  ausgrusgrb  29182  usgredg2v  29244  lfuhgr1v0e  29271  subumgredg2  29302  upgrreslem  29321  umgrreslem  29322  fusgrfisbase  29345  nbuhgr  29360  uhgrnbgr0nb  29371  nbgr0edglem  29373  nbgr1vtx  29375  cusgredg  29441  cusgrsizeinds  29470  sizusglecusg  29481  finsumvtxdg2size  29568  ewlkle  29623  upgriswlk  29659  pthdivtx  29747  dfpth2  29749  usgr2trlncl  29780  crctcshwlkn0lem4  29833  wwlksn  29857  iswwlksnon  29873  iswspthsnon  29876  wwlksm1edg  29901  wwlksnfi  29926  2pthdlem1  29950  umgr2wlk  29969  umgrclwwlkge2  30010  clwlkclwwlklem2a  30017  clwlkclwwlk  30021  clwlkclwwlkf1lem2  30024  clwlkclwwlkf  30027  clwwisshclwws  30034  clwwlknlbonbgr1  30058  clwwlknon0  30112  clwwlknonel  30114  clwwlknonex2e  30129  3pthdlem1  30183  eupth2  30258  nfrgr2v  30291  frgr3vlem1  30292  1to2vfriswmgr  30298  1to3vfriswmgr  30299  vdgn1frgrv2  30315  frgrncvvdeqlem9  30326  frgrwopreglem4a  30329  frgrregorufr0  30343  frgrregorufr  30344  2wspmdisj  30356  2clwwlk2clwwlklem  30365  frgrreggt1  30412  frgrreg  30413  frgrregord13  30415  aevdemo  30479  shsvs  31342  0cnop  31998  0cnfn  31999  cnlnssadj  32099  ssmd1  32330  ssmd2  32331  atexch  32400  mdsymlem4  32425  sumdmdlem  32437  ifeqeqx  32555  fmptcof2  32667  padct  32731  nnindf  32821  drng0mxidl  33504  constr01  33783  pwsiga  34131  pwldsys  34158  ldsysgenld  34161  fiunelros  34175  breprexp  34648  bnj151  34891  bnj594  34926  bnj600  34933  subfacp1lem6  35190  erdszelem8  35203  cvmliftlem7  35296  cvmliftlem10  35299  cvmlift2lem12  35319  sat1el2xp  35384  mrsubfval  35513  msubfval  35529  mclsssvlem  35567  funpartfv  35946  endofsegid  36086  broutsideof2  36123  a1i24  36302  nn0prpwlem  36323  nn0prpw  36324  ordcmp  36448  findreccl  36454  bj-ax6e  36669  bj-ax12v3ALT  36687  bj-xpnzex  36960  bj-ideqg1  37165  rdgssun  37379  finxp00  37403  domalom  37405  isinf2  37406  fvineqsneq  37413  wl-spae  37522  wl-nfs1t  37538  poimirlem27  37654  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  itg2addnclem3  37680  itg2addnc  37681  ftc1anc  37708  areacirclem1  37715  sdclem2  37749  fdc  37752  mettrifi  37764  isexid2  37862  zerdivemp1x  37954  smprngopr  38059  mpobi123f  38169  mptbi12f  38173  ac6s6  38179  relcnveq3  38322  mopickr  38364  elrelscnveq3  38492  disjlem14  38799  jca3  38857  ax12fromc15  38906  hbequid  38910  dvelimf-o  38930  ax12eq  38942  ax12el  38943  ax12indalem  38946  ax12inda2ALT  38947  ax12inda2  38948  lfl1dim  39122  lfl1dim2N  39123  lkreqN  39171  cvrexchlem  39421  ps-2  39480  paddasslem14  39835  idldil  40116  isltrn2N  40122  cdleme25a  40355  dibglbN  41168  dihlsscpre  41236  dvh4dimlem  41445  lcfl7N  41503  mapdval2N  41632  dvrelog2b  42067  aks6d1c6lem3  42173  monotoddzzfi  42954  onov0suclim  43287  onmcl  43344  omabs2  43345  tfsconcat0b  43359  naddgeoa  43407  rp-fakeimass  43525  clublem  43623  grur1cld  44251  ee121  44525  ee122  44526  rspsbc2  44554  ax6e2ndeq  44579  vd12  44620  vd13  44621  ee221  44670  ee212  44672  ee112  44675  ee211  44678  ee210  44680  ee201  44682  ee120  44684  ee021  44686  ee012  44688  ee102  44690  ee03  44761  ee31  44772  ee31an  44774  ee123  44783  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  refsum2cnlem1  45042  fiiuncl  45070  eliin2f  45109  disjrnmpt2  45193  disjinfi  45197  rnmptbdlem  45262  allbutfi  45404  infxrunb3rnmpt  45439  infrpgernmpt  45476  monoordxrv  45492  mccl  45613  constlimc  45639  limclner  45666  xlimmnfvlem1  45847  xlimpnfvlem1  45851  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnprodlem3  45963  stoweidlem31  46046  pwsal  46330  prsal  46333  sge0pnffigt  46411  sge0ltfirp  46415  0ome  46544  hoicvrrex  46571  hoidmvle  46615  ovnhoilem1  46616  ovnlecvr2  46625  smflimlem3  46788  ormkglobd  46890  funressnfv  47055  euoreqb  47121  ndmaovass  47218  afv2orxorb  47240  otiunsndisjX  47291  nltle2tri  47325  smonoord  47358  iccpartigtl  47410  icceuelpartlem  47422  iccpartnel  47425  sprsymrelfolem2  47480  prproropf1olem4  47493  paireqne  47498  reupr  47509  reuopreuprim  47513  fmtnoprmfac1  47552  fmtnoprmfac2  47554  prmdvdsfmtnof1lem2  47572  31prm  47584  lighneallem3  47594  lighneallem4b  47596  lighneallem4  47597  lighneal  47598  nn0o1gt2ALTV  47681  nn0oALTV  47683  odd2prm2  47705  even3prm2  47706  fpprwppr  47726  stgoldbwt  47763  sbgoldbwt  47764  sbgoldbalt  47768  sbgoldbo  47774  nnsum3primesgbe  47779  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  bgoldbtbnd  47796  bgoldbachlt  47800  tgblthelfgott  47802  dfclnbgr6  47842  grimco  47880  uhgrimisgrgric  47899  grtriprop  47908  usgrgrtrirex  47917  isubgr3stgrlem6  47938  isubgr3stgrlem8  47940  grlimgrtri  47963  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpgcubic  48035  gpg5nbgr3star  48037  upgrwlkupwlk  48056  rngccatidALTV  48188  ringccatidALTV  48222  lincdifsn  48341  lindslinindimp2lem1  48375  lindsrng01  48385  ldepsnlinc  48425  m1modmmod  48442  blen1b  48509  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  reorelicc  48631  rrx2xpref1o  48639  rrx2plord2  48643  rrxlinesc  48656  line2ylem  48672  line2xlem  48674  thincmon  49082  thincepi  49083