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  2422  ax12vALT  2468  nfsb4t  2498  moexexlem  2620  pm2.61da3ne  3015  ralrimivw  3130  rexlimdvw  3140  reximdv  3149  vtocl2d  3531  reuind  3727  reuan  3862  2reu4  4489  rabeqsnd  4636  tppreqb  4772  ssprsseq  4792  n0snor2el  4800  prnebg  4823  prel12g  4831  elpreqprlem  4833  3elpr2eq  4873  disjord  5099  disjiund  5101  dtruALT2  5328  exneq  5398  dtruOLD  5404  propssopi  5471  opthhausdorff  5480  fr0  5619  ssrel2  5751  poltletr  6108  reuop  6269  ordsssuc2  6428  ordnbtwn  6430  ndmfv  6896  fveqres  6908  fmptco  7104  funsndifnop  7126  tpres  7178  fntpb  7186  elunirn  7228  isof1oopb  7303  fvmptopabOLD  7447  ndmovord  7582  ordsucelsuc  7800  tfinds  7839  tfindsg  7840  limomss  7850  findsg  7876  finds1  7878  xpexr  7897  resf1extb  7913  bropopvvv  8072  bropfvvvvlem  8073  bropfvvvv  8074  soxp  8111  poseq  8140  suppun  8166  extmptsuppeq  8170  funsssuppss  8172  suppss  8176  suppss2  8182  suppssfv  8184  suppco  8188  mpoxopynvov0  8200  smofvon2  8328  oaordi  8513  oawordeulem  8521  odi  8546  omeulem1  8549  brdomg  8933  snmapen  9012  fopwdom  9054  fodomr  9098  mapxpen  9113  infensuc  9125  fineqvlem  9216  fineqv  9217  xpfiOLD  9277  fodomfir  9286  finsschain  9317  fsuppun  9345  fsuppunbi  9347  funsnfsupp  9350  dffi3  9389  fisup2g  9427  fisupcl  9428  fiinf2g  9460  infsupprpr  9464  wemapso2  9513  epnsym  9569  en3lplem2  9573  preleqg  9575  inf3lemd  9587  r1ordg  9738  r1val1  9746  r1pw  9805  r1pwALT  9806  rankxplim3  9841  eldju2ndl  9884  eldju2ndr  9885  carddomi2  9930  fidomtri  9953  pr2neOLD  9965  alephon  10029  alephcard  10030  alephnbtwn  10031  alephordi  10034  iunfictbso  10074  fin23lem30  10302  fin1a2lem10  10369  axdc3lem2  10411  axdc3lem4  10413  alephval2  10532  cfpwsdom  10544  axextnd  10551  axrepnd  10554  axpownd  10561  axregnd  10564  axinfndlem1  10565  fpwwe2lem11  10601  wunfi  10681  addnidpi  10861  pinq  10887  mulgt0sr  11065  dedekind  11344  nnind  12211  nn1m1nn  12214  nn0n0n1ge2b  12518  nn0lt2  12604  nn0le2is012  12605  uzm1  12838  uzinfi  12894  nn01to3  12907  xrltnsym  13104  xrlttri  13106  xrlttr  13107  qbtwnxr  13167  xltnegi  13183  xnn0xaddcl  13202  xlt2add  13227  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  reltxrnmnf  13310  fzdif1  13573  fzospliti  13659  elfzonlteqm1  13709  fzoopth  13730  elfznelfzo  13740  injresinjlem  13755  injresinj  13756  modfzo0difsn  13915  addmodlteq  13918  ssnn0fi  13957  fsuppmapnn0fiub0  13965  suppssfz  13966  seqfveq2  13996  monoord  14004  seqf1o  14015  seqhomo  14021  expnngt1  14213  faclbnd4lem4  14268  hasheqf1oi  14323  hashrabsn1  14346  hashgt0elex  14373  hash1snb  14391  hashf1lem2  14428  hashf1  14429  seqcoll  14436  hashle2pr  14449  pr2pwpr  14451  hashge2el2difr  14453  swrdnnn0nd  14628  swrdnd0  14629  pfxnd0  14660  swrdswrd  14677  pfxccatin12lem3  14704  pfxccat3  14706  swrdccat3blem  14711  repsdf2  14750  repswsymballbi  14752  cshw0  14766  cshwmodn  14767  cshwn  14769  cshwcl  14770  cshwlen  14771  cshw1  14794  2cshwcshw  14798  cshimadifsn  14802  s3sndisj  14940  s3iunsndisj  14941  relexprelg  15011  relexpnndm  15014  relexpaddg  15026  relexpaddd  15027  rtrclreclem4  15034  relexpindlem  15036  rexuz3  15322  rexanuz2  15323  limsupgre  15454  rlimconst  15517  caurcvg  15650  caucvg  15652  sumss  15697  fsumcl2lem  15704  modfsummods  15766  fsumrlim  15784  fsumo1  15785  fprodcl2lem  15923  dvdsaddre2b  16284  dvdsabseq  16290  mod2eq1n2dvds  16324  nno  16359  sumeven  16364  sumodd  16365  nn0rppwr  16538  nn0seqcvgd  16547  lcmdvds  16585  lcmfunsnlem2  16617  lcmfunsnlem  16618  divgcdcoprm0  16642  ge2nprmge4  16678  exprmfct  16681  rpexp1i  16700  prm23lt5  16792  prm23ge5  16793  pcz  16859  pcadd  16867  pcmptcl  16869  oddprmdvds  16881  prmgaplem6  17034  prmgaplem7  17035  cshwshashlem1  17073  cshwsdisj  17076  prmlem0  17083  setsstruct  17153  ressress  17224  initoeu2lem2  17984  mgm2nsgrplem2  18853  mgm2nsgrplem3  18854  dfgrp2e  18902  dfgrp3e  18979  cyccom  19142  symgextf1  19358  gsmsymgrfix  19365  gsmsymgreq  19369  sylow1lem1  19535  efgsf  19666  efgrelexlema  19686  dprdss  19968  ablfac1eulem  20011  01eq0ringOLD  20447  nrhmzr  20453  funcrngcsetcALT  20557  lssssr  20867  psgnodpm  21504  psrvscafval  21864  mplcoe1  21951  mplcoe5  21954  mpfrcl  21999  mamudm  22289  matmulcell  22339  dmatmul  22391  scmatsgrp1  22416  mavmuldm  22444  mavmulsolcl  22445  mdetunilem9  22514  cramerlem3  22583  cramer0  22584  chpscmatgsumbin  22738  chp0mat  22740  fvmptnn04ifc  22746  fvmptnn04ifd  22747  epttop  22903  neiptopnei  23026  fiuncmp  23298  1stcrest  23347  kgenss  23437  hmeofval  23652  fbun  23734  fgss2  23768  filuni  23779  filssufilg  23805  filufint  23814  hausflimi  23874  hausflim  23875  hauspwpwf1  23881  fclscmp  23924  alexsubALTlem4  23944  ptcmplem3  23948  ptcmplem5  23950  cstucnd  24178  isxmet2d  24222  imasdsf1olem  24268  blfps  24301  blf  24302  metrest  24419  nrginvrcn  24587  nmoge0  24616  nmoleub  24626  fsumcn  24768  cmetcaulem  25195  iscmet3  25200  iscmet2  25201  bcthlem2  25232  ovolicc2lem3  25427  itg2seq  25650  itg2splitlem  25656  itgeq1fOLD  25680  itgeq2  25686  iblcnlem  25697  itgfsum  25735  limcnlp  25786  perfdvf  25811  dvnres  25840  dvmptfsum  25886  c1lip1  25909  dvply2g  26199  taylply2  26282  abelth  26358  cxpsqrtth  26646  rlimcnp  26882  xrlimcnp  26885  jensen  26906  ppiublem1  27120  dchrelbas3  27156  bcmono  27195  zabsle1  27214  gausslemma2dlem0f  27279  gausslemma2dlem1a  27283  gausslemma2dlem4  27287  lgsquad2lem2  27303  2lgslem1a1  27307  2lgslem3  27322  2lgs  27325  2lgsoddprm  27334  2sqlem10  27346  2sqnn  27357  addsqnreup  27361  2sqreultblem  27366  2sqreunnltblem  27369  pntrsumbnd2  27485  pntpbnd1  27504  pntlem3  27527  nolesgn2o  27590  noetalem1  27660  bday0b  27749  leftf  27784  rightf  27785  addscutlem  27891  negscut  27952  mulscutlem  28041  n0s0suc  28241  n0sfincut  28253  n0s0m1  28259  nn1m1nns  28270  axcontlem7  28904  elntg2  28919  ausgrusgrb  29099  usgredg2v  29161  lfuhgr1v0e  29188  subumgredg2  29219  upgrreslem  29238  umgrreslem  29239  fusgrfisbase  29262  nbuhgr  29277  uhgrnbgr0nb  29288  nbgr0edglem  29290  nbgr1vtx  29292  cusgredg  29358  cusgrsizeinds  29387  sizusglecusg  29398  finsumvtxdg2size  29485  ewlkle  29540  upgriswlk  29576  pthdivtx  29664  dfpth2  29666  usgr2trlncl  29697  crctcshwlkn0lem4  29750  wwlksn  29774  iswwlksnon  29790  iswspthsnon  29793  wwlksm1edg  29818  wwlksnfi  29843  2pthdlem1  29867  umgr2wlk  29886  umgrclwwlkge2  29927  clwlkclwwlklem2a  29934  clwlkclwwlk  29938  clwlkclwwlkf1lem2  29941  clwlkclwwlkf  29944  clwwisshclwws  29951  clwwlknlbonbgr1  29975  clwwlknon0  30029  clwwlknonel  30031  clwwlknonex2e  30046  3pthdlem1  30100  eupth2  30175  nfrgr2v  30208  frgr3vlem1  30209  1to2vfriswmgr  30215  1to3vfriswmgr  30216  vdgn1frgrv2  30232  frgrncvvdeqlem9  30243  frgrwopreglem4a  30246  frgrregorufr0  30260  frgrregorufr  30261  2wspmdisj  30273  2clwwlk2clwwlklem  30282  frgrreggt1  30329  frgrreg  30330  frgrregord13  30332  aevdemo  30396  shsvs  31259  0cnop  31915  0cnfn  31916  cnlnssadj  32016  ssmd1  32247  ssmd2  32248  atexch  32317  mdsymlem4  32342  sumdmdlem  32354  ifeqeqx  32478  fmptcof2  32588  padct  32650  nnindf  32751  drng0mxidl  33454  constr01  33739  pwsiga  34127  pwldsys  34154  ldsysgenld  34157  fiunelros  34171  breprexp  34631  bnj151  34874  bnj594  34909  bnj600  34916  subfacp1lem6  35179  erdszelem8  35192  cvmliftlem7  35285  cvmliftlem10  35288  cvmlift2lem12  35308  sat1el2xp  35373  mrsubfval  35502  msubfval  35518  mclsssvlem  35556  antnestlaw2  35686  funpartfv  35940  endofsegid  36080  broutsideof2  36117  a1i24  36296  nn0prpwlem  36317  nn0prpw  36318  ordcmp  36442  findreccl  36448  bj-ax6e  36663  bj-ax12v3ALT  36681  bj-xpnzex  36954  bj-ideqg1  37159  rdgssun  37373  finxp00  37397  domalom  37399  isinf2  37400  fvineqsneq  37407  wl-spae  37516  wl-nfs1t  37532  poimirlem27  37648  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  itg2addnclem3  37674  itg2addnc  37675  ftc1anc  37702  areacirclem1  37709  sdclem2  37743  fdc  37746  mettrifi  37758  isexid2  37856  zerdivemp1x  37948  smprngopr  38053  mpobi123f  38163  mptbi12f  38167  ac6s6  38173  relcnveq3  38316  mopickr  38352  elrelscnveq3  38489  disjlem14  38797  jca3  38856  ax12fromc15  38905  hbequid  38909  dvelimf-o  38929  ax12eq  38941  ax12el  38942  ax12indalem  38945  ax12inda2ALT  38946  ax12inda2  38947  lfl1dim  39121  lfl1dim2N  39122  lkreqN  39170  cvrexchlem  39420  ps-2  39479  paddasslem14  39834  idldil  40115  isltrn2N  40121  cdleme25a  40354  dibglbN  41167  dihlsscpre  41235  dvh4dimlem  41444  lcfl7N  41502  mapdval2N  41631  dvrelog2b  42061  aks6d1c6lem3  42167  monotoddzzfi  42938  onov0suclim  43270  onmcl  43327  omabs2  43328  tfsconcat0b  43342  naddgeoa  43390  rp-fakeimass  43508  clublem  43606  grur1cld  44228  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  44737  ee31  44748  ee31an  44750  ee123  44759  ax6e2ndeqVD  44905  ax6e2ndeqALT  44927  refsum2cnlem1  45038  fiiuncl  45066  eliin2f  45105  disjrnmpt2  45189  disjinfi  45193  rnmptbdlem  45256  allbutfi  45396  infxrunb3rnmpt  45431  infrpgernmpt  45468  monoordxrv  45484  mccl  45603  constlimc  45629  limclner  45656  xlimmnfvlem1  45837  xlimpnfvlem1  45841  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnprodlem3  45953  stoweidlem31  46036  pwsal  46320  prsal  46323  sge0pnffigt  46401  sge0ltfirp  46405  0ome  46534  hoicvrrex  46561  hoidmvle  46605  ovnhoilem1  46606  ovnlecvr2  46615  smflimlem3  46778  ormkglobd  46880  funressnfv  47048  euoreqb  47114  ndmaovass  47211  afv2orxorb  47233  otiunsndisjX  47284  nltle2tri  47318  m1modmmod  47363  smonoord  47376  iccpartigtl  47428  icceuelpartlem  47440  iccpartnel  47443  sprsymrelfolem2  47498  prproropf1olem4  47511  paireqne  47516  reupr  47527  reuopreuprim  47531  fmtnoprmfac1  47570  fmtnoprmfac2  47572  prmdvdsfmtnof1lem2  47590  31prm  47602  lighneallem3  47612  lighneallem4b  47614  lighneallem4  47615  lighneal  47616  nn0o1gt2ALTV  47699  nn0oALTV  47701  odd2prm2  47723  even3prm2  47724  fpprwppr  47744  stgoldbwt  47781  sbgoldbwt  47782  sbgoldbalt  47786  sbgoldbo  47792  nnsum3primesgbe  47797  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbndlem4  47813  bgoldbtbnd  47814  bgoldbachlt  47818  tgblthelfgott  47820  dfclnbgr6  47860  grimco  47893  uhgrimisgrgric  47935  grtriprop  47944  usgrgrtrirex  47953  isubgr3stgrlem6  47974  isubgr3stgrlem8  47976  grlimgrtri  47999  gpgedg2ov  48061  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpgcubic  48074  gpg5nbgr3star  48076  gpgprismgr4cycllem7  48095  pgnbgreunbgrlem2  48111  upgrwlkupwlk  48132  rngccatidALTV  48264  ringccatidALTV  48298  lincdifsn  48417  lindslinindimp2lem1  48451  lindsrng01  48461  ldepsnlinc  48501  blen1b  48581  nn0sumshdiglemB  48613  nn0sumshdiglem1  48614  reorelicc  48703  rrx2xpref1o  48711  rrx2plord2  48715  rrxlinesc  48728  line2ylem  48744  line2xlem  48746  thincmon  49426  thincepi  49427