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  154  conax1k  173  pm2.521g2  177  pm2.61iii  187  mtod  200  imbi2d  343  adantr  483  jctild  528  jctird  529  anbi2d  630  anbi1d  631  pm3.4  808  impsingle  1628  meredith  1642  stdpc4  2073  ax12  2445  ax12vALT  2492  nfsb4t  2539  nfsb4tALT  2604  moexexlem  2711  pm2.61da3ne  3106  ralrimivw  3183  reximdv  3273  rexlimdvw  3290  vtocl2d  3557  reuind  3744  reuan  3880  rexn0  4454  2reu4  4466  tppreqb  4738  ssprsseq  4758  n0snor2el  4764  prnebg  4786  prel12g  4794  elpreqprlem  4796  3elpr2eq  4837  disjord  5054  disjiund  5056  dtru  5271  propssopi  5398  opthhausdorff  5407  fr0  5534  ssrel2  5659  poltletr  5992  reuop  6144  ordsssuc2  6279  ordnbtwn  6281  ndmfv  6700  fveqres  6712  fmptco  6891  funsndifnop  6913  tpres  6963  fntpb  6972  elunirn  7010  isof1oopb  7078  fvmptopab  7209  ndmovord  7338  ordsucelsuc  7537  tfinds  7574  tfindsg  7575  limomss  7585  findsg  7609  finds1  7611  xpexr  7623  bropopvvv  7785  bropfvvvvlem  7786  bropfvvvv  7787  soxp  7823  suppun  7850  extmptsuppeq  7854  funsssuppss  7856  suppss  7860  suppssov1  7862  suppss2  7864  suppssfv  7866  suppco  7870  mpoxopynvov0  7884  smofvon2  7993  oaordi  8172  oawordeulem  8180  odi  8205  omeulem1  8208  brdomg  8519  snmapen  8590  fopwdom  8625  fodomr  8668  mapxpen  8683  infensuc  8695  onomeneq  8708  fineqvlem  8732  fineqv  8733  xpfi  8789  finsschain  8831  fsuppun  8852  fsuppunbi  8854  funsnfsupp  8857  dffi3  8895  fisup2g  8932  fisupcl  8933  fiinf2g  8964  infsupprpr  8968  wemapso2  9017  epnsym  9072  en3lplem2  9076  preleqg  9078  inf3lemd  9090  r1ordg  9207  r1val1  9215  r1pw  9274  r1pwALT  9275  rankxplim3  9310  eldju2ndl  9353  eldju2ndr  9354  carddomi2  9399  fidomtri  9422  pr2ne  9431  alephon  9495  alephcard  9496  alephnbtwn  9497  alephordi  9500  iunfictbso  9540  fin23lem30  9764  fin1a2lem10  9831  axdc3lem2  9873  axdc3lem4  9875  alephval2  9994  cfpwsdom  10006  axextnd  10013  axrepnd  10016  axpownd  10023  axregnd  10026  axinfndlem1  10027  fpwwe2lem12  10063  wunfi  10143  addnidpi  10323  pinq  10349  mulgt0sr  10527  dedekind  10803  nnind  11656  nn1m1nn  11659  nn0n0n1ge2b  11964  nn0lt2  12046  nn0le2is012  12047  uzm1  12277  uzinfi  12329  nn01to3  12342  xrltnsym  12531  xrlttri  12533  xrlttr  12534  qbtwnxr  12594  xltnegi  12610  xnn0xaddcl  12629  xlt2add  12654  xrsupsslem  12701  xrinfmsslem  12702  xrub  12706  reltxrnmnf  12736  fzospliti  13070  elfzonlteqm1  13114  elfznelfzo  13143  injresinjlem  13158  injresinj  13159  modfzo0difsn  13312  addmodlteq  13315  ssnn0fi  13354  fsuppmapnn0fiub0  13362  suppssfz  13363  seqfveq2  13393  monoord  13401  seqf1o  13412  seqhomo  13418  expnngt1  13603  faclbnd4lem4  13657  hasheqf1oi  13713  hashrabsn1  13736  hashgt0elex  13763  hash1snb  13781  hashf1lem2  13815  hashf1  13816  seqcoll  13823  hashle2pr  13836  pr2pwpr  13838  hashge2el2difr  13840  swrdnnn0nd  14018  swrdnd0  14019  pfxnd0  14050  swrdswrd  14067  pfxccatin12lem3  14094  pfxccat3  14096  swrdccat3blem  14101  repsdf2  14140  repswsymballbi  14142  cshw0  14156  cshwmodn  14157  cshwn  14159  cshwcl  14160  cshwlen  14161  cshw1  14184  2cshwcshw  14187  cshimadifsn  14191  s3sndisj  14327  s3iunsndisj  14328  relexprelg  14397  relexpnndm  14400  relexpaddg  14412  relexpaddd  14413  rexuz3  14708  rexanuz2  14709  limsupgre  14838  rlimconst  14901  caurcvg  15033  caucvg  15035  sumss  15081  fsumcl2lem  15088  modfsummods  15148  fsumrlim  15166  fsumo1  15167  fprodcl2lem  15304  dvdsaddre2b  15657  dvdsabseq  15663  mod2eq1n2dvds  15696  nno  15733  sumeven  15738  sumodd  15739  nn0seqcvgd  15914  lcmdvds  15952  lcmfunsnlem2  15984  lcmfunsnlem  15985  divgcdcoprm0  16009  ge2nprmge4  16045  exprmfct  16048  rpexp1i  16065  prm23lt5  16151  prm23ge5  16152  pcz  16217  pcadd  16225  pcmptcl  16227  oddprmdvds  16239  prmgaplem6  16392  prmgaplem7  16393  cshwshashlem1  16429  cshwsdisj  16432  prmlem0  16439  setsstruct  16523  ressress  16562  initoeu2lem2  17275  mgm2nsgrplem2  18084  mgm2nsgrplem3  18085  dfgrp2e  18129  dfgrp3e  18199  cyccom  18346  symgextf1  18549  gsmsymgrfix  18556  gsmsymgreq  18560  sylow1lem1  18723  efgsf  18855  efgrelexlema  18875  dprdss  19151  ablfac1eulem  19194  lssssr  19725  01eq0ring  20045  psrvscafval  20170  mplcoe1  20246  mplcoe5  20249  mpfrcl  20298  psgnodpm  20732  mamudm  20999  matmulcell  21054  dmatmul  21106  scmatsgrp1  21131  mavmuldm  21159  mavmulsolcl  21160  mdetunilem9  21229  cramerlem3  21298  cramer0  21299  chpscmatgsumbin  21452  chp0mat  21454  fvmptnn04ifc  21460  fvmptnn04ifd  21461  epttop  21617  neiptopnei  21740  fiuncmp  22012  1stcrest  22061  kgenss  22151  hmeofval  22366  fbun  22448  fgss2  22482  filuni  22493  filssufilg  22519  filufint  22528  hausflimi  22588  hausflim  22589  hauspwpwf1  22595  fclscmp  22638  alexsubALTlem4  22658  ptcmplem3  22662  ptcmplem5  22664  cstucnd  22893  isxmet2d  22937  imasdsf1olem  22983  blfps  23016  blf  23017  metrest  23134  nrginvrcn  23301  nmoge0  23330  nmoleub  23340  fsumcn  23478  cmetcaulem  23891  iscmet3  23896  iscmet2  23897  bcthlem2  23928  ovolicc2lem3  24120  itg2seq  24343  itg2splitlem  24349  itgeq1f  24372  itgeq2  24378  iblcnlem  24389  itgfsum  24427  limcnlp  24476  perfdvf  24501  dvnres  24528  dvmptfsum  24572  c1lip1  24594  abelth  25029  cxpsqrtth  25312  rlimcnp  25543  xrlimcnp  25546  jensen  25566  ppiublem1  25778  dchrelbas3  25814  bcmono  25853  zabsle1  25872  gausslemma2dlem0f  25937  gausslemma2dlem1a  25941  gausslemma2dlem4  25945  lgsquad2lem2  25961  2lgslem1a1  25965  2lgslem3  25980  2lgs  25983  2lgsoddprm  25992  2sqlem10  26004  2sqnn  26015  addsqnreup  26019  2sqreultblem  26024  2sqreunnltblem  26027  pntrsumbnd2  26143  pntpbnd1  26162  pntlem3  26185  axcontlem7  26756  elntg2  26771  ausgrusgrb  26950  usgredg2v  27009  lfuhgr1v0e  27036  subumgredg2  27067  upgrreslem  27086  umgrreslem  27087  fusgrfisbase  27110  nbuhgr  27125  uhgrnbgr0nb  27136  nbgr0vtxlem  27137  nbgr1vtx  27140  cusgredg  27206  cusgrsizeinds  27234  sizusglecusg  27245  finsumvtxdg2size  27332  ewlkle  27387  upgriswlk  27422  pthdivtx  27510  usgr2trlncl  27541  crctcshwlkn0lem4  27591  wwlksn  27615  iswwlksnon  27631  iswspthsnon  27634  wwlksm1edg  27659  wwlksnfi  27684  wwlksnfiOLD  27685  2pthdlem1  27709  umgr2wlk  27728  umgrclwwlkge2  27769  clwlkclwwlklem2a  27776  clwlkclwwlk  27780  clwlkclwwlkf1lem2  27783  clwlkclwwlkf  27786  clwwisshclwws  27793  clwwlknlbonbgr1  27817  clwwlknfiOLD  27824  clwwlknon0  27872  clwwlknonel  27874  clwwlknonex2e  27889  3pthdlem1  27943  eupth2  28018  nfrgr2v  28051  frgr3vlem1  28052  1to2vfriswmgr  28058  1to3vfriswmgr  28059  vdgn1frgrv2  28075  frgrncvvdeqlem9  28086  frgrwopreglem4a  28089  frgrregorufr0  28103  frgrregorufr  28104  2wspmdisj  28116  2clwwlk2clwwlklem  28125  frgrreggt1  28172  frgrreg  28173  frgrregord13  28175  aevdemo  28239  shsvs  29100  0cnop  29756  0cnfn  29757  cnlnssadj  29857  ssmd1  30088  ssmd2  30089  atexch  30158  mdsymlem4  30183  sumdmdlem  30195  rabeqsnd  30264  ifeqeqx  30297  fmptcof2  30402  padct  30455  nnindf  30535  pwsiga  31389  pwldsys  31416  ldsysgenld  31419  fiunelros  31433  breprexp  31904  bnj151  32149  bnj594  32184  bnj600  32191  subfacp1lem6  32432  erdszelem8  32445  cvmliftlem7  32538  cvmliftlem10  32541  cvmlift2lem12  32561  sat1el2xp  32626  mrsubfval  32755  msubfval  32771  mclsssvlem  32809  trpredlem1  33066  poseq  33095  nolesgn2o  33178  funpartfv  33406  endofsegid  33546  broutsideof2  33583  a1i24  33649  nn0prpwlem  33670  nn0prpw  33671  ordcmp  33795  findreccl  33801  bj-ax6e  34001  bj-ax12v3ALT  34020  bj-dtru  34139  bj-xpnzex  34274  bj-ideqg1  34459  rdgssun  34662  finxp00  34686  domalom  34688  isinf2  34689  fvineqsneq  34696  wl-spae  34776  wl-nfs1t  34792  poimirlem27  34934  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  itg2addnclem3  34960  itg2addnc  34961  ftc1anc  34990  areacirclem1  34997  sdclem2  35032  fdc  35035  mettrifi  35047  isexid2  35148  zerdivemp1x  35240  smprngopr  35345  mpobi123f  35455  mptbi12f  35459  ac6s6  35465  relcnveq3  35593  elrelscnveq3  35746  jca3  36007  ax12fromc15  36056  hbequid  36060  dvelimf-o  36080  ax12eq  36092  ax12el  36093  ax12indalem  36096  ax12inda2ALT  36097  ax12inda2  36098  lfl1dim  36272  lfl1dim2N  36273  lkreqN  36321  cvrexchlem  36570  ps-2  36629  paddasslem14  36984  idldil  37265  isltrn2N  37271  cdleme25a  37504  dibglbN  38317  dihlsscpre  38385  dvh4dimlem  38594  lcfl7N  38652  mapdval2N  38781  sn-dtru  39160  nn0rppwr  39231  monotoddzzfi  39588  rp-fakeimass  39927  clublem  40019  relexpnul  40072  grur1cld  40617  ee121  40888  ee122  40889  rspsbc2  40917  ax6e2ndeq  40942  vd12  40983  vd13  40984  ee221  41033  ee212  41035  ee112  41038  ee211  41041  ee210  41043  ee201  41045  ee120  41047  ee021  41049  ee012  41051  ee102  41053  ee03  41124  ee31  41135  ee31an  41137  ee123  41146  ax6e2ndeqVD  41292  ax6e2ndeqALT  41314  refsum2cnlem1  41343  fiiuncl  41376  eliin2f  41419  disjrnmpt2  41498  disjinfi  41503  rnmptbdlem  41576  allbutfi  41714  infxrunb3rnmpt  41751  infrpgernmpt  41790  monoordxrv  41807  mccl  41928  constlimc  41954  limclner  41981  xlimmnfvlem1  42162  xlimpnfvlem1  42166  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvmptfprod  42279  dvnprodlem3  42282  stoweidlem31  42365  pwsal  42649  prsal  42652  sge0pnffigt  42727  sge0ltfirp  42731  0ome  42860  hoicvrrex  42887  hoidmvle  42931  ovnhoilem1  42932  ovnlecvr2  42941  smflimlem3  43098  funressnfv  43327  euoreqb  43357  ndmaovass  43454  afv2orxorb  43476  otiunsndisjX  43527  nltle2tri  43562  fzoopth  43576  smonoord  43580  iccpartigtl  43632  icceuelpartlem  43644  iccpartnel  43647  sprsymrelfolem2  43704  prproropf1olem4  43717  paireqne  43722  reupr  43733  reuopreuprim  43737  fmtnoprmfac1  43776  fmtnoprmfac2  43778  prmdvdsfmtnof1lem2  43796  31prm  43809  lighneallem3  43821  lighneallem4b  43823  lighneallem4  43824  lighneal  43825  nn0o1gt2ALTV  43908  nn0oALTV  43910  odd2prm2  43932  even3prm2  43933  fpprwppr  43953  stgoldbwt  43990  sbgoldbwt  43991  sbgoldbalt  43995  sbgoldbo  44001  nnsum3primesgbe  44006  wtgoldbnnsum4prm  44016  bgoldbnnsum3prm  44018  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  bgoldbtbnd  44023  bgoldbachlt  44027  tgblthelfgott  44029  upgrwlkupwlk  44064  nrhmzr  44193  rngccatidALTV  44309  funcrngcsetcALT  44319  ringccatidALTV  44372  lincdifsn  44528  lindslinindimp2lem1  44562  lindsrng01  44572  ldepsnlinc  44612  m1modmmod  44630  blen1b  44697  nn0sumshdiglemB  44729  nn0sumshdiglem1  44730  reorelicc  44746  rrx2xpref1o  44754  rrx2plord2  44758  rrxlinesc  44771  line2ylem  44787  line2xlem  44789