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  2068  ax12  2427  ax12vALT  2473  nfsb4t  2503  moexexlem  2625  pm2.61da3ne  3021  ralrimivw  3136  rexlimdvw  3146  reximdv  3155  vtocl2d  3541  reuind  3736  reuan  3871  2reu4  4498  rabeqsnd  4645  tppreqb  4781  ssprsseq  4801  n0snor2el  4809  prnebg  4832  prel12g  4840  elpreqprlem  4842  3elpr2eq  4882  disjord  5108  disjiund  5110  dtruALT2  5340  exneq  5410  dtruOLD  5416  propssopi  5483  opthhausdorff  5492  fr0  5632  ssrel2  5764  poltletr  6121  reuop  6282  ordsssuc2  6444  ordnbtwn  6446  ndmfv  6910  fveqres  6922  fmptco  7118  funsndifnop  7140  tpres  7192  fntpb  7200  elunirn  7242  isof1oopb  7317  fvmptopabOLD  7460  ndmovord  7595  ordsucelsuc  7814  tfinds  7853  tfindsg  7854  limomss  7864  findsg  7891  finds1  7893  xpexr  7912  resf1extb  7928  bropopvvv  8087  bropfvvvvlem  8088  bropfvvvv  8089  soxp  8126  poseq  8155  suppun  8181  extmptsuppeq  8185  funsssuppss  8187  suppss  8191  suppss2  8197  suppssfv  8199  suppco  8203  mpoxopynvov0  8215  smofvon2  8368  oaordi  8556  oawordeulem  8564  odi  8589  omeulem1  8592  brdomg  8969  brdomgOLD  8970  snmapen  9050  fopwdom  9092  fodomr  9140  mapxpen  9155  infensuc  9167  onomeneqOLD  9236  fineqvlem  9268  fineqv  9269  xpfiOLD  9329  fodomfir  9338  finsschain  9369  fsuppun  9397  fsuppunbi  9399  funsnfsupp  9402  dffi3  9441  fisup2g  9479  fisupcl  9480  fiinf2g  9512  infsupprpr  9516  wemapso2  9565  epnsym  9621  en3lplem2  9625  preleqg  9627  inf3lemd  9639  r1ordg  9790  r1val1  9798  r1pw  9857  r1pwALT  9858  rankxplim3  9893  eldju2ndl  9936  eldju2ndr  9937  carddomi2  9982  fidomtri  10005  pr2neOLD  10017  alephon  10081  alephcard  10082  alephnbtwn  10083  alephordi  10086  iunfictbso  10126  fin23lem30  10354  fin1a2lem10  10421  axdc3lem2  10463  axdc3lem4  10465  alephval2  10584  cfpwsdom  10596  axextnd  10603  axrepnd  10606  axpownd  10613  axregnd  10616  axinfndlem1  10617  fpwwe2lem11  10653  wunfi  10733  addnidpi  10913  pinq  10939  mulgt0sr  11117  dedekind  11396  nnind  12256  nn1m1nn  12259  nn0n0n1ge2b  12568  nn0lt2  12654  nn0le2is012  12655  uzm1  12888  uzinfi  12942  nn01to3  12955  xrltnsym  13151  xrlttri  13153  xrlttr  13154  qbtwnxr  13214  xltnegi  13230  xnn0xaddcl  13249  xlt2add  13274  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  reltxrnmnf  13357  fzdif1  13620  fzospliti  13706  elfzonlteqm1  13755  fzoopth  13776  elfznelfzo  13786  injresinjlem  13801  injresinj  13802  modfzo0difsn  13959  addmodlteq  13962  ssnn0fi  14001  fsuppmapnn0fiub0  14009  suppssfz  14010  seqfveq2  14040  monoord  14048  seqf1o  14059  seqhomo  14065  expnngt1  14257  faclbnd4lem4  14312  hasheqf1oi  14367  hashrabsn1  14390  hashgt0elex  14417  hash1snb  14435  hashf1lem2  14472  hashf1  14473  seqcoll  14480  hashle2pr  14493  pr2pwpr  14495  hashge2el2difr  14497  swrdnnn0nd  14672  swrdnd0  14673  pfxnd0  14704  swrdswrd  14721  pfxccatin12lem3  14748  pfxccat3  14750  swrdccat3blem  14755  repsdf2  14794  repswsymballbi  14796  cshw0  14810  cshwmodn  14811  cshwn  14813  cshwcl  14814  cshwlen  14815  cshw1  14838  2cshwcshw  14842  cshimadifsn  14846  s3sndisj  14984  s3iunsndisj  14985  relexprelg  15055  relexpnndm  15058  relexpaddg  15070  relexpaddd  15071  rtrclreclem4  15078  relexpindlem  15080  rexuz3  15365  rexanuz2  15366  limsupgre  15495  rlimconst  15558  caurcvg  15691  caucvg  15693  sumss  15738  fsumcl2lem  15745  modfsummods  15807  fsumrlim  15825  fsumo1  15826  fprodcl2lem  15964  dvdsaddre2b  16324  dvdsabseq  16330  mod2eq1n2dvds  16364  nno  16399  sumeven  16404  sumodd  16405  nn0rppwr  16578  nn0seqcvgd  16587  lcmdvds  16625  lcmfunsnlem2  16657  lcmfunsnlem  16658  divgcdcoprm0  16682  ge2nprmge4  16718  exprmfct  16721  rpexp1i  16740  prm23lt5  16832  prm23ge5  16833  pcz  16899  pcadd  16907  pcmptcl  16909  oddprmdvds  16921  prmgaplem6  17074  prmgaplem7  17075  cshwshashlem1  17113  cshwsdisj  17116  prmlem0  17123  setsstruct  17193  ressress  17266  initoeu2lem2  18026  mgm2nsgrplem2  18895  mgm2nsgrplem3  18896  dfgrp2e  18944  dfgrp3e  19021  cyccom  19184  symgextf1  19400  gsmsymgrfix  19407  gsmsymgreq  19411  sylow1lem1  19577  efgsf  19708  efgrelexlema  19728  dprdss  20010  ablfac1eulem  20053  01eq0ringOLD  20489  nrhmzr  20495  funcrngcsetcALT  20599  lssssr  20909  psgnodpm  21546  psrvscafval  21906  mplcoe1  21993  mplcoe5  21996  mpfrcl  22041  mamudm  22331  matmulcell  22381  dmatmul  22433  scmatsgrp1  22458  mavmuldm  22486  mavmulsolcl  22487  mdetunilem9  22556  cramerlem3  22625  cramer0  22626  chpscmatgsumbin  22780  chp0mat  22782  fvmptnn04ifc  22788  fvmptnn04ifd  22789  epttop  22945  neiptopnei  23068  fiuncmp  23340  1stcrest  23389  kgenss  23479  hmeofval  23694  fbun  23776  fgss2  23810  filuni  23821  filssufilg  23847  filufint  23856  hausflimi  23916  hausflim  23917  hauspwpwf1  23923  fclscmp  23966  alexsubALTlem4  23986  ptcmplem3  23990  ptcmplem5  23992  cstucnd  24220  isxmet2d  24264  imasdsf1olem  24310  blfps  24343  blf  24344  metrest  24461  nrginvrcn  24629  nmoge0  24658  nmoleub  24668  fsumcn  24810  cmetcaulem  25238  iscmet3  25243  iscmet2  25244  bcthlem2  25275  ovolicc2lem3  25470  itg2seq  25693  itg2splitlem  25699  itgeq1fOLD  25723  itgeq2  25729  iblcnlem  25740  itgfsum  25778  limcnlp  25829  perfdvf  25854  dvnres  25883  dvmptfsum  25929  c1lip1  25952  dvply2g  26242  taylply2  26325  abelth  26401  cxpsqrtth  26689  rlimcnp  26925  xrlimcnp  26928  jensen  26949  ppiublem1  27163  dchrelbas3  27199  bcmono  27238  zabsle1  27257  gausslemma2dlem0f  27322  gausslemma2dlem1a  27326  gausslemma2dlem4  27330  lgsquad2lem2  27346  2lgslem1a1  27350  2lgslem3  27365  2lgs  27368  2lgsoddprm  27377  2sqlem10  27389  2sqnn  27400  addsqnreup  27404  2sqreultblem  27409  2sqreunnltblem  27412  pntrsumbnd2  27528  pntpbnd1  27547  pntlem3  27570  nolesgn2o  27633  noetalem1  27703  bday0b  27792  leftf  27821  rightf  27822  addscutlem  27927  negscut  27988  mulscutlem  28074  n0s0suc  28262  n0s0m1  28276  axcontlem7  28895  elntg2  28910  ausgrusgrb  29090  usgredg2v  29152  lfuhgr1v0e  29179  subumgredg2  29210  upgrreslem  29229  umgrreslem  29230  fusgrfisbase  29253  nbuhgr  29268  uhgrnbgr0nb  29279  nbgr0edglem  29281  nbgr1vtx  29283  cusgredg  29349  cusgrsizeinds  29378  sizusglecusg  29389  finsumvtxdg2size  29476  ewlkle  29531  upgriswlk  29567  pthdivtx  29655  dfpth2  29657  usgr2trlncl  29688  crctcshwlkn0lem4  29741  wwlksn  29765  iswwlksnon  29781  iswspthsnon  29784  wwlksm1edg  29809  wwlksnfi  29834  2pthdlem1  29858  umgr2wlk  29877  umgrclwwlkge2  29918  clwlkclwwlklem2a  29925  clwlkclwwlk  29929  clwlkclwwlkf1lem2  29932  clwlkclwwlkf  29935  clwwisshclwws  29942  clwwlknlbonbgr1  29966  clwwlknon0  30020  clwwlknonel  30022  clwwlknonex2e  30037  3pthdlem1  30091  eupth2  30166  nfrgr2v  30199  frgr3vlem1  30200  1to2vfriswmgr  30206  1to3vfriswmgr  30207  vdgn1frgrv2  30223  frgrncvvdeqlem9  30234  frgrwopreglem4a  30237  frgrregorufr0  30251  frgrregorufr  30252  2wspmdisj  30264  2clwwlk2clwwlklem  30273  frgrreggt1  30320  frgrreg  30321  frgrregord13  30323  aevdemo  30387  shsvs  31250  0cnop  31906  0cnfn  31907  cnlnssadj  32007  ssmd1  32238  ssmd2  32239  atexch  32308  mdsymlem4  32333  sumdmdlem  32345  ifeqeqx  32469  fmptcof2  32581  padct  32643  nnindf  32744  drng0mxidl  33437  constr01  33722  pwsiga  34107  pwldsys  34134  ldsysgenld  34137  fiunelros  34151  breprexp  34611  bnj151  34854  bnj594  34889  bnj600  34896  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  36265  nn0prpwlem  36286  nn0prpw  36287  ordcmp  36411  findreccl  36417  bj-ax6e  36632  bj-ax12v3ALT  36650  bj-xpnzex  36923  bj-ideqg1  37128  rdgssun  37342  finxp00  37366  domalom  37368  isinf2  37369  fvineqsneq  37376  wl-spae  37485  wl-nfs1t  37501  poimirlem27  37617  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  itg2addnclem3  37643  itg2addnc  37644  ftc1anc  37671  areacirclem1  37678  sdclem2  37712  fdc  37715  mettrifi  37727  isexid2  37825  zerdivemp1x  37917  smprngopr  38022  mpobi123f  38132  mptbi12f  38136  ac6s6  38142  relcnveq3  38285  mopickr  38327  elrelscnveq3  38455  disjlem14  38762  jca3  38820  ax12fromc15  38869  hbequid  38873  dvelimf-o  38893  ax12eq  38905  ax12el  38906  ax12indalem  38909  ax12inda2ALT  38910  ax12inda2  38911  lfl1dim  39085  lfl1dim2N  39086  lkreqN  39134  cvrexchlem  39384  ps-2  39443  paddasslem14  39798  idldil  40079  isltrn2N  40085  cdleme25a  40318  dibglbN  41131  dihlsscpre  41199  dvh4dimlem  41408  lcfl7N  41466  mapdval2N  41595  dvrelog2b  42025  aks6d1c6lem3  42131  monotoddzzfi  42913  onov0suclim  43245  onmcl  43302  omabs2  43303  tfsconcat0b  43317  naddgeoa  43365  rp-fakeimass  43483  clublem  43581  grur1cld  44204  ee121  44478  ee122  44479  rspsbc2  44507  ax6e2ndeq  44532  vd12  44573  vd13  44574  ee221  44623  ee212  44625  ee112  44628  ee211  44631  ee210  44633  ee201  44635  ee120  44637  ee021  44639  ee012  44641  ee102  44643  ee03  44713  ee31  44724  ee31an  44726  ee123  44735  ax6e2ndeqVD  44881  ax6e2ndeqALT  44903  refsum2cnlem1  45009  fiiuncl  45037  eliin2f  45076  disjrnmpt2  45160  disjinfi  45164  rnmptbdlem  45227  allbutfi  45368  infxrunb3rnmpt  45403  infrpgernmpt  45440  monoordxrv  45456  mccl  45575  constlimc  45601  limclner  45628  xlimmnfvlem1  45809  xlimpnfvlem1  45813  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnprodlem3  45925  stoweidlem31  46008  pwsal  46292  prsal  46295  sge0pnffigt  46373  sge0ltfirp  46377  0ome  46506  hoicvrrex  46533  hoidmvle  46577  ovnhoilem1  46578  ovnlecvr2  46587  smflimlem3  46750  ormkglobd  46852  funressnfv  47020  euoreqb  47086  ndmaovass  47183  afv2orxorb  47205  otiunsndisjX  47256  nltle2tri  47290  smonoord  47333  iccpartigtl  47385  icceuelpartlem  47397  iccpartnel  47400  sprsymrelfolem2  47455  prproropf1olem4  47468  paireqne  47473  reupr  47484  reuopreuprim  47488  fmtnoprmfac1  47527  fmtnoprmfac2  47529  prmdvdsfmtnof1lem2  47547  31prm  47559  lighneallem3  47569  lighneallem4b  47571  lighneallem4  47572  lighneal  47573  nn0o1gt2ALTV  47656  nn0oALTV  47658  odd2prm2  47680  even3prm2  47681  fpprwppr  47701  stgoldbwt  47738  sbgoldbwt  47739  sbgoldbalt  47743  sbgoldbo  47749  nnsum3primesgbe  47754  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbndlem4  47770  bgoldbtbnd  47771  bgoldbachlt  47775  tgblthelfgott  47777  dfclnbgr6  47817  grimco  47850  uhgrimisgrgric  47892  grtriprop  47901  usgrgrtrirex  47910  isubgr3stgrlem6  47931  isubgr3stgrlem8  47933  grlimgrtri  47956  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpgcubic  48029  gpg5nbgr3star  48031  gpgprismgr4cycllem7  48048  upgrwlkupwlk  48063  rngccatidALTV  48195  ringccatidALTV  48229  lincdifsn  48348  lindslinindimp2lem1  48382  lindsrng01  48392  ldepsnlinc  48432  m1modmmod  48449  blen1b  48516  nn0sumshdiglemB  48548  nn0sumshdiglem1  48549  reorelicc  48638  rrx2xpref1o  48646  rrx2plord2  48650  rrxlinesc  48663  line2ylem  48679  line2xlem  48681  thincmon  49267  thincepi  49268