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  197  imbi2d  340  adantr  481  jctild  526  jctird  527  anbi2d  629  anbi1d  630  pm3.4  808  impsingle  1629  meredith  1643  stdpc4  2071  ax12  2421  ax12vALT  2467  nfsb4t  2497  moexexlem  2621  pm2.61da3ne  3030  ralrimivw  3143  rexlimdvw  3153  reximdv  3163  vtocl2d  3514  reuind  3714  reuan  3855  rexn0OLD  4477  2reu4  4489  tppreqb  4770  ssprsseq  4790  n0snor2el  4796  prnebg  4818  prel12g  4826  elpreqprlem  4828  3elpr2eq  4869  disjord  5098  disjiund  5100  dtruALT2  5330  exneq  5397  dtruOLD  5403  propssopi  5470  opthhausdorff  5479  fr0  5617  ssrel2  5746  poltletr  6091  reuop  6250  ordsssuc2  6413  ordnbtwn  6415  ndmfv  6882  fveqres  6894  fmptco  7080  funsndifnop  7102  tpres  7155  fntpb  7164  elunirn  7203  isof1oopb  7275  fvmptopabOLD  7417  ndmovord  7549  ordsucelsuc  7762  tfinds  7801  tfindsg  7802  limomss  7812  findsg  7841  finds1  7843  xpexr  7860  bropopvvv  8027  bropfvvvvlem  8028  bropfvvvv  8029  soxp  8066  poseq  8095  suppun  8120  extmptsuppeq  8124  funsssuppss  8126  suppss  8130  suppssOLD  8131  suppssov1  8134  suppss2  8136  suppssfv  8138  suppco  8142  mpoxopynvov0  8154  smofvon2  8307  oaordi  8498  oawordeulem  8506  odi  8531  omeulem1  8534  brdomg  8903  brdomgOLD  8904  snmapen  8989  fopwdom  9031  fodomr  9079  mapxpen  9094  infensuc  9106  onomeneqOLD  9180  fineqvlem  9213  fineqv  9214  xpfiOLD  9269  finsschain  9310  fsuppun  9333  fsuppunbi  9335  funsnfsupp  9338  dffi3  9376  fisup2g  9413  fisupcl  9414  fiinf2g  9445  infsupprpr  9449  wemapso2  9498  epnsym  9554  en3lplem2  9558  preleqg  9560  inf3lemd  9572  r1ordg  9723  r1val1  9731  r1pw  9790  r1pwALT  9791  rankxplim3  9826  eldju2ndl  9869  eldju2ndr  9870  carddomi2  9915  fidomtri  9938  pr2neOLD  9950  alephon  10014  alephcard  10015  alephnbtwn  10016  alephordi  10019  iunfictbso  10059  fin23lem30  10287  fin1a2lem10  10354  axdc3lem2  10396  axdc3lem4  10398  alephval2  10517  cfpwsdom  10529  axextnd  10536  axrepnd  10539  axpownd  10546  axregnd  10549  axinfndlem1  10550  fpwwe2lem11  10586  wunfi  10666  addnidpi  10846  pinq  10872  mulgt0sr  11050  dedekind  11327  nnind  12180  nn1m1nn  12183  nn0n0n1ge2b  12490  nn0lt2  12575  nn0le2is012  12576  uzm1  12810  uzinfi  12862  nn01to3  12875  xrltnsym  13066  xrlttri  13068  xrlttr  13069  qbtwnxr  13129  xltnegi  13145  xnn0xaddcl  13164  xlt2add  13189  xrsupsslem  13236  xrinfmsslem  13237  xrub  13241  reltxrnmnf  13271  fzospliti  13614  elfzonlteqm1  13658  elfznelfzo  13687  injresinjlem  13702  injresinj  13703  modfzo0difsn  13858  addmodlteq  13861  ssnn0fi  13900  fsuppmapnn0fiub0  13908  suppssfz  13909  seqfveq2  13940  monoord  13948  seqf1o  13959  seqhomo  13965  expnngt1  14154  faclbnd4lem4  14206  hasheqf1oi  14261  hashrabsn1  14284  hashgt0elex  14311  hash1snb  14329  hashf1lem2  14367  hashf1  14368  seqcoll  14375  hashle2pr  14388  pr2pwpr  14390  hashge2el2difr  14392  swrdnnn0nd  14556  swrdnd0  14557  pfxnd0  14588  swrdswrd  14605  pfxccatin12lem3  14632  pfxccat3  14634  swrdccat3blem  14639  repsdf2  14678  repswsymballbi  14680  cshw0  14694  cshwmodn  14695  cshwn  14697  cshwcl  14698  cshwlen  14699  cshw1  14722  2cshwcshw  14726  cshimadifsn  14730  s3sndisj  14864  s3iunsndisj  14865  relexprelg  14935  relexpnndm  14938  relexpaddg  14950  relexpaddd  14951  rtrclreclem4  14958  relexpindlem  14960  rexuz3  15245  rexanuz2  15246  limsupgre  15375  rlimconst  15438  caurcvg  15573  caucvg  15575  sumss  15620  fsumcl2lem  15627  modfsummods  15689  fsumrlim  15707  fsumo1  15708  fprodcl2lem  15844  dvdsaddre2b  16200  dvdsabseq  16206  mod2eq1n2dvds  16240  nno  16275  sumeven  16280  sumodd  16281  nn0seqcvgd  16457  lcmdvds  16495  lcmfunsnlem2  16527  lcmfunsnlem  16528  divgcdcoprm0  16552  ge2nprmge4  16588  exprmfct  16591  rpexp1i  16610  prm23lt5  16697  prm23ge5  16698  pcz  16764  pcadd  16772  pcmptcl  16774  oddprmdvds  16786  prmgaplem6  16939  prmgaplem7  16940  cshwshashlem1  16979  cshwsdisj  16982  prmlem0  16989  setsstruct  17059  ressress  17143  initoeu2lem2  17915  mgm2nsgrplem2  18743  mgm2nsgrplem3  18744  dfgrp2e  18790  dfgrp3e  18861  cyccom  19010  symgextf1  19217  gsmsymgrfix  19224  gsmsymgreq  19228  sylow1lem1  19394  efgsf  19525  efgrelexlema  19545  dprdss  19822  ablfac1eulem  19865  01eq0ringOLD  20216  lssssr  20471  psgnodpm  21029  psrvscafval  21395  mplcoe1  21475  mplcoe5  21478  mpfrcl  21532  mamudm  21774  matmulcell  21831  dmatmul  21883  scmatsgrp1  21908  mavmuldm  21936  mavmulsolcl  21937  mdetunilem9  22006  cramerlem3  22075  cramer0  22076  chpscmatgsumbin  22230  chp0mat  22232  fvmptnn04ifc  22238  fvmptnn04ifd  22239  epttop  22396  neiptopnei  22520  fiuncmp  22792  1stcrest  22841  kgenss  22931  hmeofval  23146  fbun  23228  fgss2  23262  filuni  23273  filssufilg  23299  filufint  23308  hausflimi  23368  hausflim  23369  hauspwpwf1  23375  fclscmp  23418  alexsubALTlem4  23438  ptcmplem3  23442  ptcmplem5  23444  cstucnd  23673  isxmet2d  23717  imasdsf1olem  23763  blfps  23796  blf  23797  metrest  23917  nrginvrcn  24093  nmoge0  24122  nmoleub  24132  fsumcn  24270  cmetcaulem  24689  iscmet3  24694  iscmet2  24695  bcthlem2  24726  ovolicc2lem3  24920  itg2seq  25144  itg2splitlem  25150  itgeq1f  25173  itgeq2  25179  iblcnlem  25190  itgfsum  25228  limcnlp  25279  perfdvf  25304  dvnres  25332  dvmptfsum  25376  c1lip1  25398  abelth  25837  cxpsqrtth  26121  rlimcnp  26352  xrlimcnp  26355  jensen  26375  ppiublem1  26587  dchrelbas3  26623  bcmono  26662  zabsle1  26681  gausslemma2dlem0f  26746  gausslemma2dlem1a  26750  gausslemma2dlem4  26754  lgsquad2lem2  26770  2lgslem1a1  26774  2lgslem3  26789  2lgs  26792  2lgsoddprm  26801  2sqlem10  26813  2sqnn  26824  addsqnreup  26828  2sqreultblem  26833  2sqreunnltblem  26836  pntrsumbnd2  26952  pntpbnd1  26971  pntlem3  26994  nolesgn2o  27056  noetalem1  27126  bday0b  27212  leftf  27238  rightf  27239  addscut  27332  negscut  27380  axcontlem7  27982  elntg2  27997  ausgrusgrb  28179  usgredg2v  28238  lfuhgr1v0e  28265  subumgredg2  28296  upgrreslem  28315  umgrreslem  28316  fusgrfisbase  28339  nbuhgr  28354  uhgrnbgr0nb  28365  nbgr0vtxlem  28366  nbgr1vtx  28369  cusgredg  28435  cusgrsizeinds  28463  sizusglecusg  28474  finsumvtxdg2size  28561  ewlkle  28616  upgriswlk  28652  pthdivtx  28740  usgr2trlncl  28771  crctcshwlkn0lem4  28821  wwlksn  28845  iswwlksnon  28861  iswspthsnon  28864  wwlksm1edg  28889  wwlksnfi  28914  2pthdlem1  28938  umgr2wlk  28957  umgrclwwlkge2  28998  clwlkclwwlklem2a  29005  clwlkclwwlk  29009  clwlkclwwlkf1lem2  29012  clwlkclwwlkf  29015  clwwisshclwws  29022  clwwlknlbonbgr1  29046  clwwlknon0  29100  clwwlknonel  29102  clwwlknonex2e  29117  3pthdlem1  29171  eupth2  29246  nfrgr2v  29279  frgr3vlem1  29280  1to2vfriswmgr  29286  1to3vfriswmgr  29287  vdgn1frgrv2  29303  frgrncvvdeqlem9  29314  frgrwopreglem4a  29317  frgrregorufr0  29331  frgrregorufr  29332  2wspmdisj  29344  2clwwlk2clwwlklem  29353  frgrreggt1  29400  frgrreg  29401  frgrregord13  29403  aevdemo  29467  shsvs  30328  0cnop  30984  0cnfn  30985  cnlnssadj  31085  ssmd1  31316  ssmd2  31317  atexch  31386  mdsymlem4  31411  sumdmdlem  31423  rabeqsnd  31493  ifeqeqx  31528  fmptcof2  31640  padct  31704  nnindf  31785  pwsiga  32818  pwldsys  32845  ldsysgenld  32848  fiunelros  32862  breprexp  33335  bnj151  33578  bnj594  33613  bnj600  33620  subfacp1lem6  33866  erdszelem8  33879  cvmliftlem7  33972  cvmliftlem10  33975  cvmlift2lem12  33995  sat1el2xp  34060  mrsubfval  34189  msubfval  34205  mclsssvlem  34243  funpartfv  34606  endofsegid  34746  broutsideof2  34783  a1i24  34849  nn0prpwlem  34870  nn0prpw  34871  ordcmp  34995  findreccl  35001  bj-ax6e  35208  bj-ax12v3ALT  35227  bj-xpnzex  35503  bj-ideqg1  35708  rdgssun  35922  finxp00  35946  domalom  35948  isinf2  35949  fvineqsneq  35956  wl-spae  36053  wl-nfs1t  36069  poimirlem27  36178  ovoliunnfl  36193  voliunnfl  36195  volsupnfl  36196  itg2addnclem3  36204  itg2addnc  36205  ftc1anc  36232  areacirclem1  36239  sdclem2  36274  fdc  36277  mettrifi  36289  isexid2  36387  zerdivemp1x  36479  smprngopr  36584  mpobi123f  36694  mptbi12f  36698  ac6s6  36704  relcnveq3  36855  mopickr  36897  elrelscnveq3  37026  disjlem14  37333  jca3  37391  ax12fromc15  37440  hbequid  37444  dvelimf-o  37464  ax12eq  37476  ax12el  37477  ax12indalem  37480  ax12inda2ALT  37481  ax12inda2  37482  lfl1dim  37656  lfl1dim2N  37657  lkreqN  37705  cvrexchlem  37955  ps-2  38014  paddasslem14  38369  idldil  38650  isltrn2N  38656  cdleme25a  38889  dibglbN  39702  dihlsscpre  39770  dvh4dimlem  39979  lcfl7N  40037  mapdval2N  40166  dvrelog2b  40596  nn0rppwr  40877  monotoddzzfi  41324  onov0suclim  41667  onmcl  41724  omabs2  41725  tfsconcat0b  41739  naddgeoa  41788  rp-fakeimass  41906  clublem  42004  grur1cld  42634  ee121  42909  ee122  42910  rspsbc2  42938  ax6e2ndeq  42963  vd12  43004  vd13  43005  ee221  43054  ee212  43056  ee112  43059  ee211  43062  ee210  43064  ee201  43066  ee120  43068  ee021  43070  ee012  43072  ee102  43074  ee03  43145  ee31  43156  ee31an  43158  ee123  43167  ax6e2ndeqVD  43313  ax6e2ndeqALT  43335  refsum2cnlem1  43364  fiiuncl  43395  eliin2f  43436  disjrnmpt2  43529  disjinfi  43534  rnmptbdlem  43604  allbutfi  43748  infxrunb3rnmpt  43783  infrpgernmpt  43820  monoordxrv  43837  mccl  43959  constlimc  43985  limclner  44012  xlimmnfvlem1  44193  xlimpnfvlem1  44197  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  dvmptfprod  44306  dvnprodlem3  44309  stoweidlem31  44392  pwsal  44676  prsal  44679  sge0pnffigt  44757  sge0ltfirp  44761  0ome  44890  hoicvrrex  44917  hoidmvle  44961  ovnhoilem1  44962  ovnlecvr2  44971  smflimlem3  45134  funressnfv  45397  euoreqb  45461  ndmaovass  45558  afv2orxorb  45580  otiunsndisjX  45631  nltle2tri  45665  fzoopth  45679  smonoord  45683  iccpartigtl  45735  icceuelpartlem  45747  iccpartnel  45750  sprsymrelfolem2  45805  prproropf1olem4  45818  paireqne  45823  reupr  45834  reuopreuprim  45838  fmtnoprmfac1  45877  fmtnoprmfac2  45879  prmdvdsfmtnof1lem2  45897  31prm  45909  lighneallem3  45919  lighneallem4b  45921  lighneallem4  45922  lighneal  45923  nn0o1gt2ALTV  46006  nn0oALTV  46008  odd2prm2  46030  even3prm2  46031  fpprwppr  46051  stgoldbwt  46088  sbgoldbwt  46089  sbgoldbalt  46093  sbgoldbo  46099  nnsum3primesgbe  46104  wtgoldbnnsum4prm  46114  bgoldbnnsum3prm  46116  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  bgoldbtbndlem4  46120  bgoldbtbnd  46121  bgoldbachlt  46125  tgblthelfgott  46127  upgrwlkupwlk  46162  nrhmzr  46291  rngccatidALTV  46407  funcrngcsetcALT  46417  ringccatidALTV  46470  lincdifsn  46625  lindslinindimp2lem1  46659  lindsrng01  46669  ldepsnlinc  46709  m1modmmod  46727  blen1b  46794  nn0sumshdiglemB  46826  nn0sumshdiglem1  46827  reorelicc  46916  rrx2xpref1o  46924  rrx2plord2  46928  rrxlinesc  46941  line2ylem  46957  line2xlem  46959  thincmon  47174  thincepi  47175