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  2427  ax12vALT  2473  nfsb4t  2503  moexexlem  2626  pm2.61da3ne  3021  ralrimivw  3132  rexlimdvw  3142  reximdv  3151  vtocl2d  3519  reuind  3711  reuan  3846  2reu4  4477  rabeqsnd  4626  tppreqb  4761  ssprsseq  4781  n0snor2el  4789  prnebg  4812  prel12g  4820  elpreqprlem  4822  3elpr2eq  4862  disjord  5087  disjiund  5089  dtruALT2  5315  exneq  5385  propssopi  5456  opthhausdorff  5465  fr0  5602  ssrel2  5734  poltletr  6089  reuop  6251  ordsssuc2  6410  ordnbtwn  6412  ndmfv  6866  fveqres  6878  fmptco  7074  funsndifnop  7096  tpres  7147  fntpb  7155  elunirn  7197  isof1oopb  7271  ndmovord  7548  ordsucelsuc  7764  tfinds  7802  tfindsg  7803  limomss  7813  findsg  7839  finds1  7841  xpexr  7860  resf1extb  7876  bropopvvv  8032  bropfvvvvlem  8033  bropfvvvv  8034  soxp  8071  poseq  8100  suppun  8126  extmptsuppeq  8130  funsssuppss  8132  suppss  8136  suppss2  8142  suppssfv  8144  suppco  8148  mpoxopynvov0  8160  smofvon2  8288  oaordi  8473  oawordeulem  8481  odi  8506  omeulem1  8509  brdomg  8895  snmapen  8975  fopwdom  9013  fodomr  9056  mapxpen  9071  infensuc  9083  fineqvlem  9166  fineqv  9167  fodomfir  9228  finsschain  9259  fsuppun  9290  fsuppunbi  9292  funsnfsupp  9295  dffi3  9334  fisup2g  9372  fisupcl  9373  fiinf2g  9405  infsupprpr  9409  wemapso2  9458  epnsym  9518  en3lplem2  9522  preleqg  9524  inf3lemd  9536  r1ordg  9690  r1val1  9698  r1pw  9757  r1pwALT  9758  rankxplim3  9793  eldju2ndl  9836  eldju2ndr  9837  carddomi2  9882  fidomtri  9905  alephon  9979  alephcard  9980  alephnbtwn  9981  alephordi  9984  iunfictbso  10024  fin23lem30  10252  fin1a2lem10  10319  axdc3lem2  10361  axdc3lem4  10363  alephval2  10483  cfpwsdom  10495  axextnd  10502  axrepnd  10505  axpownd  10512  axregnd  10515  axinfndlem1  10516  fpwwe2lem11  10552  wunfi  10632  addnidpi  10812  pinq  10838  mulgt0sr  11016  dedekind  11296  nnind  12163  nn1m1nn  12166  nn0n0n1ge2b  12470  nn0lt2  12555  nn0le2is012  12556  uzm1  12785  uzinfi  12841  nn01to3  12854  xrltnsym  13051  xrlttri  13053  xrlttr  13054  qbtwnxr  13115  xltnegi  13131  xnn0xaddcl  13150  xlt2add  13175  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  reltxrnmnf  13258  fzdif1  13521  fzospliti  13607  elfzonlteqm1  13657  fzoopth  13678  elfznelfzo  13689  injresinjlem  13706  injresinj  13707  modfzo0difsn  13866  addmodlteq  13869  ssnn0fi  13908  fsuppmapnn0fiub0  13916  suppssfz  13917  seqfveq2  13947  monoord  13955  seqf1o  13966  seqhomo  13972  expnngt1  14164  faclbnd4lem4  14219  hasheqf1oi  14274  hashrabsn1  14297  hashgt0elex  14324  hash1snb  14342  hashf1lem2  14379  hashf1  14380  seqcoll  14387  hashle2pr  14400  pr2pwpr  14402  hashge2el2difr  14404  swrdnnn0nd  14580  swrdnd0  14581  pfxnd0  14612  swrdswrd  14628  pfxccatin12lem3  14655  pfxccat3  14657  swrdccat3blem  14662  repsdf2  14701  repswsymballbi  14703  cshw0  14717  cshwmodn  14718  cshwn  14720  cshwcl  14721  cshwlen  14722  cshw1  14745  2cshwcshw  14748  cshimadifsn  14752  s3sndisj  14890  s3iunsndisj  14891  relexprelg  14961  relexpnndm  14964  relexpaddg  14976  relexpaddd  14977  rtrclreclem4  14984  relexpindlem  14986  rexuz3  15272  rexanuz2  15273  limsupgre  15404  rlimconst  15467  caurcvg  15600  caucvg  15602  sumss  15647  fsumcl2lem  15654  modfsummods  15716  fsumrlim  15734  fsumo1  15735  fprodcl2lem  15873  dvdsaddre2b  16234  dvdsabseq  16240  mod2eq1n2dvds  16274  nno  16309  sumeven  16314  sumodd  16315  nn0rppwr  16488  nn0seqcvgd  16497  lcmdvds  16535  lcmfunsnlem2  16567  lcmfunsnlem  16568  divgcdcoprm0  16592  ge2nprmge4  16628  exprmfct  16631  rpexp1i  16650  prm23lt5  16742  prm23ge5  16743  pcz  16809  pcadd  16817  pcmptcl  16819  oddprmdvds  16831  prmgaplem6  16984  prmgaplem7  16985  cshwshashlem1  17023  cshwsdisj  17026  prmlem0  17033  setsstruct  17103  ressress  17174  initoeu2lem2  17939  mgm2nsgrplem2  18844  mgm2nsgrplem3  18845  dfgrp2e  18893  dfgrp3e  18970  cyccom  19132  symgextf1  19350  gsmsymgrfix  19357  gsmsymgreq  19361  sylow1lem1  19527  efgsf  19658  efgrelexlema  19678  dprdss  19960  ablfac1eulem  20003  01eq0ringOLD  20464  nrhmzr  20470  funcrngcsetcALT  20574  lssssr  20905  psgnodpm  21543  psrvscafval  21904  mplcoe1  21992  mplcoe5  21995  mpfrcl  22040  mamudm  22339  matmulcell  22389  dmatmul  22441  scmatsgrp1  22466  mavmuldm  22494  mavmulsolcl  22495  mdetunilem9  22564  cramerlem3  22633  cramer0  22634  chpscmatgsumbin  22788  chp0mat  22790  fvmptnn04ifc  22796  fvmptnn04ifd  22797  epttop  22953  neiptopnei  23076  fiuncmp  23348  1stcrest  23397  kgenss  23487  hmeofval  23702  fbun  23784  fgss2  23818  filuni  23829  filssufilg  23855  filufint  23864  hausflimi  23924  hausflim  23925  hauspwpwf1  23931  fclscmp  23974  alexsubALTlem4  23994  ptcmplem3  23998  ptcmplem5  24000  cstucnd  24227  isxmet2d  24271  imasdsf1olem  24317  blfps  24350  blf  24351  metrest  24468  nrginvrcn  24636  nmoge0  24665  nmoleub  24675  fsumcn  24817  cmetcaulem  25244  iscmet3  25249  iscmet2  25250  bcthlem2  25281  ovolicc2lem3  25476  itg2seq  25699  itg2splitlem  25705  itgeq1fOLD  25729  itgeq2  25735  iblcnlem  25746  itgfsum  25784  limcnlp  25835  perfdvf  25860  dvnres  25889  dvmptfsum  25935  c1lip1  25958  dvply2g  26248  taylply2  26331  abelth  26407  cxpsqrtth  26695  rlimcnp  26931  xrlimcnp  26934  jensen  26955  ppiublem1  27169  dchrelbas3  27205  bcmono  27244  zabsle1  27263  gausslemma2dlem0f  27328  gausslemma2dlem1a  27332  gausslemma2dlem4  27336  lgsquad2lem2  27352  2lgslem1a1  27356  2lgslem3  27371  2lgs  27374  2lgsoddprm  27383  2sqlem10  27395  2sqnn  27406  addsqnreup  27410  2sqreultblem  27415  2sqreunnltblem  27418  pntrsumbnd2  27534  pntpbnd1  27553  pntlem3  27576  nolesgn2o  27639  noetalem1  27709  bday0b  27809  leftf  27851  rightf  27852  oldss  27866  addcutslem  27973  negcut  28035  mulcutlem  28127  n0s0suc  28338  n0fincut  28351  n0s0m1  28358  nn1m1nns  28370  axcontlem7  29043  elntg2  29058  ausgrusgrb  29238  usgredg2v  29300  lfuhgr1v0e  29327  subumgredg2  29358  upgrreslem  29377  umgrreslem  29378  fusgrfisbase  29401  nbuhgr  29416  uhgrnbgr0nb  29427  nbgr0edglem  29429  nbgr1vtx  29431  cusgredg  29497  cusgrsizeinds  29526  sizusglecusg  29537  finsumvtxdg2size  29624  ewlkle  29679  upgriswlk  29714  pthdivtx  29800  dfpth2  29802  usgr2trlncl  29833  crctcshwlkn0lem4  29886  wwlksn  29910  iswwlksnon  29926  iswspthsnon  29929  wwlksm1edg  29954  wwlksnfi  29979  2pthdlem1  30003  umgr2wlk  30022  umgrclwwlkge2  30066  clwlkclwwlklem2a  30073  clwlkclwwlk  30077  clwlkclwwlkf1lem2  30080  clwlkclwwlkf  30083  clwwisshclwws  30090  clwwlknlbonbgr1  30114  clwwlknon0  30168  clwwlknonel  30170  clwwlknonex2e  30185  3pthdlem1  30239  eupth2  30314  nfrgr2v  30347  frgr3vlem1  30348  1to2vfriswmgr  30354  1to3vfriswmgr  30355  vdgn1frgrv2  30371  frgrncvvdeqlem9  30382  frgrwopreglem4a  30385  frgrregorufr0  30399  frgrregorufr  30400  2wspmdisj  30412  2clwwlk2clwwlklem  30421  frgrreggt1  30468  frgrreg  30469  frgrregord13  30471  aevdemo  30535  shsvs  31398  0cnop  32054  0cnfn  32055  cnlnssadj  32155  ssmd1  32386  ssmd2  32387  atexch  32456  mdsymlem4  32481  sumdmdlem  32493  ifeqeqx  32617  fmptcof2  32735  padct  32797  nnindf  32900  drng0mxidl  33557  constr01  33899  pwsiga  34287  pwldsys  34314  ldsysgenld  34317  fiunelros  34331  breprexp  34790  bnj151  35033  bnj594  35068  bnj600  35075  trssfir1om  35267  trssfir1omregs  35292  subfacp1lem6  35379  erdszelem8  35392  cvmliftlem7  35485  cvmliftlem10  35488  cvmlift2lem12  35508  sat1el2xp  35573  mrsubfval  35702  msubfval  35718  mclsssvlem  35756  antnestlaw2  35886  funpartfv  36139  endofsegid  36279  broutsideof2  36316  a1i24  36495  nn0prpwlem  36516  nn0prpw  36517  ordcmp  36641  findreccl  36647  bj-ax6e  36869  bj-ax12v3ALT  36887  bj-xpnzex  37160  bj-ideqg1  37365  rdgssun  37579  finxp00  37603  domalom  37605  isinf2  37606  fvineqsneq  37613  wl-spae  37722  wl-nfs1t  37738  poimirlem27  37844  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  itg2addnclem3  37870  itg2addnc  37871  ftc1anc  37898  areacirclem1  37905  sdclem2  37939  fdc  37942  mettrifi  37954  isexid2  38052  zerdivemp1x  38144  smprngopr  38249  mpobi123f  38359  mptbi12f  38363  ac6s6  38369  relcnveq3  38516  mopickr  38552  elrelscnveq3  38796  disjlem14  39053  jca3  39112  ax12fromc15  39161  hbequid  39165  dvelimf-o  39185  ax12eq  39197  ax12el  39198  ax12indalem  39201  ax12inda2ALT  39202  ax12inda2  39203  lfl1dim  39377  lfl1dim2N  39378  lkreqN  39426  cvrexchlem  39675  ps-2  39734  paddasslem14  40089  idldil  40370  isltrn2N  40376  cdleme25a  40609  dibglbN  41422  dihlsscpre  41490  dvh4dimlem  41699  lcfl7N  41757  mapdval2N  41886  dvrelog2b  42316  aks6d1c6lem3  42422  monotoddzzfi  43180  onov0suclim  43512  onmcl  43569  omabs2  43570  tfsconcat0b  43584  naddgeoa  43632  rp-fakeimass  43749  clublem  43847  grur1cld  44469  ee121  44742  ee122  44743  rspsbc2  44771  ax6e2ndeq  44796  vd12  44837  vd13  44838  ee221  44887  ee212  44889  ee112  44892  ee211  44895  ee210  44897  ee201  44899  ee120  44901  ee021  44903  ee012  44905  ee102  44907  ee03  44977  ee31  44988  ee31an  44990  ee123  44999  ax6e2ndeqVD  45145  ax6e2ndeqALT  45167  refsum2cnlem1  45278  fiiuncl  45306  eliin2f  45344  disjrnmpt2  45428  disjinfi  45432  rnmptbdlem  45495  allbutfi  45633  infxrunb3rnmpt  45668  infrpgernmpt  45705  monoordxrv  45721  mccl  45840  constlimc  45866  limclner  45891  xlimmnfvlem1  46072  xlimpnfvlem1  46076  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvnprodlem3  46188  stoweidlem31  46271  pwsal  46555  prsal  46558  sge0pnffigt  46636  sge0ltfirp  46640  0ome  46769  hoicvrrex  46796  hoidmvle  46840  ovnhoilem1  46841  ovnlecvr2  46850  smflimlem3  47013  ormkglobd  47115  chnsubseqword  47118  funressnfv  47285  euoreqb  47351  ndmaovass  47448  afv2orxorb  47470  otiunsndisjX  47521  nltle2tri  47555  m1modmmod  47600  smonoord  47613  iccpartigtl  47665  icceuelpartlem  47677  iccpartnel  47680  sprsymrelfolem2  47735  prproropf1olem4  47748  paireqne  47753  reupr  47764  reuopreuprim  47768  fmtnoprmfac1  47807  fmtnoprmfac2  47809  prmdvdsfmtnof1lem2  47827  31prm  47839  lighneallem3  47849  lighneallem4b  47851  lighneallem4  47852  lighneal  47853  nn0o1gt2ALTV  47936  nn0oALTV  47938  odd2prm2  47960  even3prm2  47961  fpprwppr  47981  stgoldbwt  48018  sbgoldbwt  48019  sbgoldbalt  48023  sbgoldbo  48029  nnsum3primesgbe  48034  wtgoldbnnsum4prm  48044  bgoldbnnsum3prm  48046  bgoldbtbndlem2  48048  bgoldbtbndlem3  48049  bgoldbtbndlem4  48050  bgoldbtbnd  48051  bgoldbachlt  48055  tgblthelfgott  48057  dfclnbgr6  48098  grimco  48131  uhgrimisgrgric  48173  grtriprop  48183  usgrgrtrirex  48192  isubgr3stgrlem6  48213  isubgr3stgrlem8  48215  grlimprclnbgr  48238  grlimgrtri  48245  gpgedg2ov  48308  gpg5nbgrvtx03starlem1  48310  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx03starlem3  48312  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem2  48314  gpg5nbgrvtx13starlem3  48315  gpgcubic  48321  gpg5nbgr3star  48323  gpgprismgr4cycllem7  48343  pgnbgreunbgrlem2  48359  gpg5edgnedg  48372  upgrwlkupwlk  48382  rngccatidALTV  48514  ringccatidALTV  48548  lincdifsn  48666  lindslinindimp2lem1  48700  lindsrng01  48710  ldepsnlinc  48750  blen1b  48830  nn0sumshdiglemB  48862  nn0sumshdiglem1  48863  reorelicc  48952  rrx2xpref1o  48960  rrx2plord2  48964  rrxlinesc  48977  line2ylem  48993  line2xlem  48995  thincmon  49674  thincepi  49675