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  480  jctild  525  jctird  526  anbi2d  628  anbi1d  629  pm3.4  806  impsingle  1631  meredith  1645  stdpc4  2072  ax12  2423  ax12vALT  2469  nfsb4t  2503  moexexlem  2628  pm2.61da3ne  3033  ralrimivw  3108  reximdv  3201  rexlimdvw  3218  vtocl2d  3486  reuind  3683  reuan  3825  rexn0OLD  4442  2reu4  4454  tppreqb  4735  ssprsseq  4755  n0snor2el  4761  prnebg  4783  prel12g  4791  elpreqprlem  4793  3elpr2eq  4835  disjord  5058  disjiund  5060  dtru  5288  propssopi  5416  opthhausdorff  5425  fr0  5559  ssrel2  5685  poltletr  6026  reuop  6185  ordsssuc2  6339  ordnbtwn  6341  ndmfv  6786  fveqres  6798  fmptco  6983  funsndifnop  7005  tpres  7058  fntpb  7067  elunirn  7106  isof1oopb  7176  fvmptopab  7308  ndmovord  7440  ordsucelsuc  7644  tfinds  7681  tfindsg  7682  limomss  7692  findsg  7720  finds1  7722  xpexr  7739  bropopvvv  7901  bropfvvvvlem  7902  bropfvvvv  7903  soxp  7941  suppun  7971  extmptsuppeq  7975  funsssuppss  7977  suppss  7981  suppssOLD  7982  suppssov1  7985  suppss2  7987  suppssfv  7989  suppco  7993  mpoxopynvov0  8005  smofvon2  8158  oaordi  8339  oawordeulem  8347  odi  8372  omeulem1  8375  brdomg  8703  snmapen  8782  fopwdom  8820  fodomr  8864  mapxpen  8879  infensuc  8891  onomeneq  8943  fineqvlem  8966  fineqv  8967  xpfi  9015  finsschain  9056  fsuppun  9077  fsuppunbi  9079  funsnfsupp  9082  dffi3  9120  fisup2g  9157  fisupcl  9158  fiinf2g  9189  infsupprpr  9193  wemapso2  9242  epnsym  9297  en3lplem2  9301  preleqg  9303  inf3lemd  9315  trpredlem1  9405  r1ordg  9467  r1val1  9475  r1pw  9534  r1pwALT  9535  rankxplim3  9570  eldju2ndl  9613  eldju2ndr  9614  carddomi2  9659  fidomtri  9682  pr2ne  9692  alephon  9756  alephcard  9757  alephnbtwn  9758  alephordi  9761  iunfictbso  9801  fin23lem30  10029  fin1a2lem10  10096  axdc3lem2  10138  axdc3lem4  10140  alephval2  10259  cfpwsdom  10271  axextnd  10278  axrepnd  10281  axpownd  10288  axregnd  10291  axinfndlem1  10292  fpwwe2lem11  10328  wunfi  10408  addnidpi  10588  pinq  10614  mulgt0sr  10792  dedekind  11068  nnind  11921  nn1m1nn  11924  nn0n0n1ge2b  12231  nn0lt2  12313  nn0le2is012  12314  uzm1  12545  uzinfi  12597  nn01to3  12610  xrltnsym  12800  xrlttri  12802  xrlttr  12803  qbtwnxr  12863  xltnegi  12879  xnn0xaddcl  12898  xlt2add  12923  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  reltxrnmnf  13005  fzospliti  13347  elfzonlteqm1  13391  elfznelfzo  13420  injresinjlem  13435  injresinj  13436  modfzo0difsn  13591  addmodlteq  13594  ssnn0fi  13633  fsuppmapnn0fiub0  13641  suppssfz  13642  seqfveq2  13673  monoord  13681  seqf1o  13692  seqhomo  13698  expnngt1  13884  faclbnd4lem4  13938  hasheqf1oi  13994  hashrabsn1  14017  hashgt0elex  14044  hash1snb  14062  hashf1lem2  14098  hashf1  14099  seqcoll  14106  hashle2pr  14119  pr2pwpr  14121  hashge2el2difr  14123  swrdnnn0nd  14297  swrdnd0  14298  pfxnd0  14329  swrdswrd  14346  pfxccatin12lem3  14373  pfxccat3  14375  swrdccat3blem  14380  repsdf2  14419  repswsymballbi  14421  cshw0  14435  cshwmodn  14436  cshwn  14438  cshwcl  14439  cshwlen  14440  cshw1  14463  2cshwcshw  14466  cshimadifsn  14470  s3sndisj  14606  s3iunsndisj  14607  relexprelg  14677  relexpnndm  14680  relexpaddg  14692  relexpaddd  14693  rtrclreclem4  14700  relexpindlem  14702  rexuz3  14988  rexanuz2  14989  limsupgre  15118  rlimconst  15181  caurcvg  15316  caucvg  15318  sumss  15364  fsumcl2lem  15371  modfsummods  15433  fsumrlim  15451  fsumo1  15452  fprodcl2lem  15588  dvdsaddre2b  15944  dvdsabseq  15950  mod2eq1n2dvds  15984  nno  16019  sumeven  16024  sumodd  16025  nn0seqcvgd  16203  lcmdvds  16241  lcmfunsnlem2  16273  lcmfunsnlem  16274  divgcdcoprm0  16298  ge2nprmge4  16334  exprmfct  16337  rpexp1i  16356  prm23lt5  16443  prm23ge5  16444  pcz  16510  pcadd  16518  pcmptcl  16520  oddprmdvds  16532  prmgaplem6  16685  prmgaplem7  16686  cshwshashlem1  16725  cshwsdisj  16728  prmlem0  16735  setsstruct  16805  ressress  16884  initoeu2lem2  17646  mgm2nsgrplem2  18473  mgm2nsgrplem3  18474  dfgrp2e  18520  dfgrp3e  18590  cyccom  18737  symgextf1  18944  gsmsymgrfix  18951  gsmsymgreq  18955  sylow1lem1  19118  efgsf  19250  efgrelexlema  19270  dprdss  19547  ablfac1eulem  19590  lssssr  20130  01eq0ring  20456  psgnodpm  20705  psrvscafval  21069  mplcoe1  21148  mplcoe5  21151  mpfrcl  21205  mamudm  21447  matmulcell  21502  dmatmul  21554  scmatsgrp1  21579  mavmuldm  21607  mavmulsolcl  21608  mdetunilem9  21677  cramerlem3  21746  cramer0  21747  chpscmatgsumbin  21901  chp0mat  21903  fvmptnn04ifc  21909  fvmptnn04ifd  21910  epttop  22067  neiptopnei  22191  fiuncmp  22463  1stcrest  22512  kgenss  22602  hmeofval  22817  fbun  22899  fgss2  22933  filuni  22944  filssufilg  22970  filufint  22979  hausflimi  23039  hausflim  23040  hauspwpwf1  23046  fclscmp  23089  alexsubALTlem4  23109  ptcmplem3  23113  ptcmplem5  23115  cstucnd  23344  isxmet2d  23388  imasdsf1olem  23434  blfps  23467  blf  23468  metrest  23586  nrginvrcn  23762  nmoge0  23791  nmoleub  23801  fsumcn  23939  cmetcaulem  24357  iscmet3  24362  iscmet2  24363  bcthlem2  24394  ovolicc2lem3  24588  itg2seq  24812  itg2splitlem  24818  itgeq1f  24841  itgeq2  24847  iblcnlem  24858  itgfsum  24896  limcnlp  24947  perfdvf  24972  dvnres  25000  dvmptfsum  25044  c1lip1  25066  abelth  25505  cxpsqrtth  25789  rlimcnp  26020  xrlimcnp  26023  jensen  26043  ppiublem1  26255  dchrelbas3  26291  bcmono  26330  zabsle1  26349  gausslemma2dlem0f  26414  gausslemma2dlem1a  26418  gausslemma2dlem4  26422  lgsquad2lem2  26438  2lgslem1a1  26442  2lgslem3  26457  2lgs  26460  2lgsoddprm  26469  2sqlem10  26481  2sqnn  26492  addsqnreup  26496  2sqreultblem  26501  2sqreunnltblem  26504  pntrsumbnd2  26620  pntpbnd1  26639  pntlem3  26662  axcontlem7  27241  elntg2  27256  ausgrusgrb  27438  usgredg2v  27497  lfuhgr1v0e  27524  subumgredg2  27555  upgrreslem  27574  umgrreslem  27575  fusgrfisbase  27598  nbuhgr  27613  uhgrnbgr0nb  27624  nbgr0vtxlem  27625  nbgr1vtx  27628  cusgredg  27694  cusgrsizeinds  27722  sizusglecusg  27733  finsumvtxdg2size  27820  ewlkle  27875  upgriswlk  27910  pthdivtx  27998  usgr2trlncl  28029  crctcshwlkn0lem4  28079  wwlksn  28103  iswwlksnon  28119  iswspthsnon  28122  wwlksm1edg  28147  wwlksnfi  28172  2pthdlem1  28196  umgr2wlk  28215  umgrclwwlkge2  28256  clwlkclwwlklem2a  28263  clwlkclwwlk  28267  clwlkclwwlkf1lem2  28270  clwlkclwwlkf  28273  clwwisshclwws  28280  clwwlknlbonbgr1  28304  clwwlknon0  28358  clwwlknonel  28360  clwwlknonex2e  28375  3pthdlem1  28429  eupth2  28504  nfrgr2v  28537  frgr3vlem1  28538  1to2vfriswmgr  28544  1to3vfriswmgr  28545  vdgn1frgrv2  28561  frgrncvvdeqlem9  28572  frgrwopreglem4a  28575  frgrregorufr0  28589  frgrregorufr  28590  2wspmdisj  28602  2clwwlk2clwwlklem  28611  frgrreggt1  28658  frgrreg  28659  frgrregord13  28661  aevdemo  28725  shsvs  29586  0cnop  30242  0cnfn  30243  cnlnssadj  30343  ssmd1  30574  ssmd2  30575  atexch  30644  mdsymlem4  30669  sumdmdlem  30681  rabeqsnd  30749  ifeqeqx  30786  fmptcof2  30896  padct  30956  nnindf  31035  pwsiga  31998  pwldsys  32025  ldsysgenld  32028  fiunelros  32042  breprexp  32513  bnj151  32757  bnj594  32792  bnj600  32799  subfacp1lem6  33047  erdszelem8  33060  cvmliftlem7  33153  cvmliftlem10  33156  cvmlift2lem12  33176  sat1el2xp  33241  mrsubfval  33370  msubfval  33386  mclsssvlem  33424  poxp3  33723  poseq  33729  nolesgn2o  33801  noetalem1  33871  bday0b  33951  leftf  33976  rightf  33977  funpartfv  34174  endofsegid  34314  broutsideof2  34351  a1i24  34417  nn0prpwlem  34438  nn0prpw  34439  ordcmp  34563  findreccl  34569  bj-ax6e  34776  bj-ax12v3ALT  34795  bj-dtru  34926  bj-xpnzex  35076  bj-ideqg1  35262  rdgssun  35476  finxp00  35500  domalom  35502  isinf2  35503  fvineqsneq  35510  wl-spae  35607  wl-nfs1t  35623  poimirlem27  35731  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  itg2addnclem3  35757  itg2addnc  35758  ftc1anc  35785  areacirclem1  35792  sdclem2  35827  fdc  35830  mettrifi  35842  isexid2  35940  zerdivemp1x  36032  smprngopr  36137  mpobi123f  36247  mptbi12f  36251  ac6s6  36257  relcnveq3  36383  elrelscnveq3  36536  jca3  36797  ax12fromc15  36846  hbequid  36850  dvelimf-o  36870  ax12eq  36882  ax12el  36883  ax12indalem  36886  ax12inda2ALT  36887  ax12inda2  36888  lfl1dim  37062  lfl1dim2N  37063  lkreqN  37111  cvrexchlem  37360  ps-2  37419  paddasslem14  37774  idldil  38055  isltrn2N  38061  cdleme25a  38294  dibglbN  39107  dihlsscpre  39175  dvh4dimlem  39384  lcfl7N  39442  mapdval2N  39571  dvrelog2b  40002  sn-dtru  40116  nn0rppwr  40254  monotoddzzfi  40680  rp-fakeimass  41017  clublem  41107  relexpnul  41175  grur1cld  41739  ee121  42014  ee122  42015  rspsbc2  42043  ax6e2ndeq  42068  vd12  42109  vd13  42110  ee221  42159  ee212  42161  ee112  42164  ee211  42167  ee210  42169  ee201  42171  ee120  42173  ee021  42175  ee012  42177  ee102  42179  ee03  42250  ee31  42261  ee31an  42263  ee123  42272  ax6e2ndeqVD  42418  ax6e2ndeqALT  42440  refsum2cnlem1  42469  fiiuncl  42502  eliin2f  42543  disjrnmpt2  42615  disjinfi  42620  rnmptbdlem  42690  allbutfi  42823  infxrunb3rnmpt  42858  infrpgernmpt  42895  monoordxrv  42912  mccl  43029  constlimc  43055  limclner  43082  xlimmnfvlem1  43263  xlimpnfvlem1  43267  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvmptfprod  43376  dvnprodlem3  43379  stoweidlem31  43462  pwsal  43746  prsal  43749  sge0pnffigt  43824  sge0ltfirp  43828  0ome  43957  hoicvrrex  43984  hoidmvle  44028  ovnhoilem1  44029  ovnlecvr2  44038  smflimlem3  44195  funressnfv  44424  euoreqb  44488  ndmaovass  44585  afv2orxorb  44607  otiunsndisjX  44658  nltle2tri  44693  fzoopth  44707  smonoord  44711  iccpartigtl  44763  icceuelpartlem  44775  iccpartnel  44778  sprsymrelfolem2  44833  prproropf1olem4  44846  paireqne  44851  reupr  44862  reuopreuprim  44866  fmtnoprmfac1  44905  fmtnoprmfac2  44907  prmdvdsfmtnof1lem2  44925  31prm  44937  lighneallem3  44947  lighneallem4b  44949  lighneallem4  44950  lighneal  44951  nn0o1gt2ALTV  45034  nn0oALTV  45036  odd2prm2  45058  even3prm2  45059  fpprwppr  45079  stgoldbwt  45116  sbgoldbwt  45117  sbgoldbalt  45121  sbgoldbo  45127  nnsum3primesgbe  45132  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbndlem4  45148  bgoldbtbnd  45149  bgoldbachlt  45153  tgblthelfgott  45155  upgrwlkupwlk  45190  nrhmzr  45319  rngccatidALTV  45435  funcrngcsetcALT  45445  ringccatidALTV  45498  lincdifsn  45653  lindslinindimp2lem1  45687  lindsrng01  45697  ldepsnlinc  45737  m1modmmod  45755  blen1b  45822  nn0sumshdiglemB  45854  nn0sumshdiglem1  45855  reorelicc  45944  rrx2xpref1o  45952  rrx2plord2  45956  rrxlinesc  45969  line2ylem  45985  line2xlem  45987  thincmon  46203  thincepi  46204