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  809  impsingle  1622  meredith  1636  stdpc4  2064  ax12  2417  ax12vALT  2463  nfsb4t  2493  moexexlem  2617  pm2.61da3ne  3026  ralrimivw  3145  rexlimdvw  3155  reximdv  3165  vtocl2d  3545  reuind  3746  reuan  3886  rexn0OLD  4510  2reu4  4522  rabeqsnd  4667  tppreqb  4804  ssprsseq  4824  n0snor2el  4830  prnebg  4852  prel12g  4860  elpreqprlem  4862  3elpr2eq  4902  disjord  5130  disjiund  5132  dtruALT2  5364  exneq  5431  dtruOLD  5437  propssopi  5504  opthhausdorff  5513  fr0  5651  ssrel2  5781  poltletr  6132  reuop  6291  ordsssuc2  6454  ordnbtwn  6456  ndmfv  6926  fveqres  6938  fmptco  7132  funsndifnop  7154  tpres  7207  fntpb  7215  elunirn  7255  isof1oopb  7327  fvmptopabOLD  7469  ndmovord  7605  ordsucelsuc  7819  tfinds  7858  tfindsg  7859  limomss  7869  findsg  7899  finds1  7901  xpexr  7920  bropopvvv  8089  bropfvvvvlem  8090  bropfvvvv  8091  soxp  8128  poseq  8157  suppun  8182  extmptsuppeq  8186  funsssuppss  8188  suppss  8192  suppssOLD  8193  suppss2  8199  suppssfv  8201  suppco  8205  mpoxopynvov0  8217  smofvon2  8370  oaordi  8560  oawordeulem  8568  odi  8593  omeulem1  8596  brdomg  8968  brdomgOLD  8969  snmapen  9054  fopwdom  9096  fodomr  9144  mapxpen  9159  infensuc  9171  onomeneqOLD  9245  fineqvlem  9278  fineqv  9279  xpfiOLD  9334  finsschain  9375  fsuppun  9402  fsuppunbi  9404  funsnfsupp  9407  dffi3  9446  fisup2g  9483  fisupcl  9484  fiinf2g  9515  infsupprpr  9519  wemapso2  9568  epnsym  9624  en3lplem2  9628  preleqg  9630  inf3lemd  9642  r1ordg  9793  r1val1  9801  r1pw  9860  r1pwALT  9861  rankxplim3  9896  eldju2ndl  9939  eldju2ndr  9940  carddomi2  9985  fidomtri  10008  pr2neOLD  10020  alephon  10084  alephcard  10085  alephnbtwn  10086  alephordi  10089  iunfictbso  10129  fin23lem30  10357  fin1a2lem10  10424  axdc3lem2  10466  axdc3lem4  10468  alephval2  10587  cfpwsdom  10599  axextnd  10606  axrepnd  10609  axpownd  10616  axregnd  10619  axinfndlem1  10620  fpwwe2lem11  10656  wunfi  10736  addnidpi  10916  pinq  10942  mulgt0sr  11120  dedekind  11399  nnind  12252  nn1m1nn  12255  nn0n0n1ge2b  12562  nn0lt2  12647  nn0le2is012  12648  uzm1  12882  uzinfi  12934  nn01to3  12947  xrltnsym  13140  xrlttri  13142  xrlttr  13143  qbtwnxr  13203  xltnegi  13219  xnn0xaddcl  13238  xlt2add  13263  xrsupsslem  13310  xrinfmsslem  13311  xrub  13315  reltxrnmnf  13345  fzospliti  13688  elfzonlteqm1  13732  elfznelfzo  13761  injresinjlem  13776  injresinj  13777  modfzo0difsn  13932  addmodlteq  13935  ssnn0fi  13974  fsuppmapnn0fiub0  13982  suppssfz  13983  seqfveq2  14013  monoord  14021  seqf1o  14032  seqhomo  14038  expnngt1  14227  faclbnd4lem4  14279  hasheqf1oi  14334  hashrabsn1  14357  hashgt0elex  14384  hash1snb  14402  hashf1lem2  14441  hashf1  14442  seqcoll  14449  hashle2pr  14462  pr2pwpr  14464  hashge2el2difr  14466  swrdnnn0nd  14630  swrdnd0  14631  pfxnd0  14662  swrdswrd  14679  pfxccatin12lem3  14706  pfxccat3  14708  swrdccat3blem  14713  repsdf2  14752  repswsymballbi  14754  cshw0  14768  cshwmodn  14769  cshwn  14771  cshwcl  14772  cshwlen  14773  cshw1  14796  2cshwcshw  14800  cshimadifsn  14804  s3sndisj  14938  s3iunsndisj  14939  relexprelg  15009  relexpnndm  15012  relexpaddg  15024  relexpaddd  15025  rtrclreclem4  15032  relexpindlem  15034  rexuz3  15319  rexanuz2  15320  limsupgre  15449  rlimconst  15512  caurcvg  15647  caucvg  15649  sumss  15694  fsumcl2lem  15701  modfsummods  15763  fsumrlim  15781  fsumo1  15782  fprodcl2lem  15918  dvdsaddre2b  16275  dvdsabseq  16281  mod2eq1n2dvds  16315  nno  16350  sumeven  16355  sumodd  16356  nn0seqcvgd  16532  lcmdvds  16570  lcmfunsnlem2  16602  lcmfunsnlem  16603  divgcdcoprm0  16627  ge2nprmge4  16663  exprmfct  16666  rpexp1i  16686  prm23lt5  16774  prm23ge5  16775  pcz  16841  pcadd  16849  pcmptcl  16851  oddprmdvds  16863  prmgaplem6  17016  prmgaplem7  17017  cshwshashlem1  17056  cshwsdisj  17059  prmlem0  17066  setsstruct  17136  ressress  17220  initoeu2lem2  17995  mgm2nsgrplem2  18862  mgm2nsgrplem3  18863  dfgrp2e  18911  dfgrp3e  18987  cyccom  19149  symgextf1  19367  gsmsymgrfix  19374  gsmsymgreq  19378  sylow1lem1  19544  efgsf  19675  efgrelexlema  19695  dprdss  19977  ablfac1eulem  20020  01eq0ringOLD  20457  nrhmzr  20463  funcrngcsetcALT  20563  lssssr  20827  psgnodpm  21507  psrvscafval  21878  mplcoe1  21962  mplcoe5  21965  mpfrcl  22018  mamudm  22277  matmulcell  22334  dmatmul  22386  scmatsgrp1  22411  mavmuldm  22439  mavmulsolcl  22440  mdetunilem9  22509  cramerlem3  22578  cramer0  22579  chpscmatgsumbin  22733  chp0mat  22735  fvmptnn04ifc  22741  fvmptnn04ifd  22742  epttop  22899  neiptopnei  23023  fiuncmp  23295  1stcrest  23344  kgenss  23434  hmeofval  23649  fbun  23731  fgss2  23765  filuni  23776  filssufilg  23802  filufint  23811  hausflimi  23871  hausflim  23872  hauspwpwf1  23878  fclscmp  23921  alexsubALTlem4  23941  ptcmplem3  23945  ptcmplem5  23947  cstucnd  24176  isxmet2d  24220  imasdsf1olem  24266  blfps  24299  blf  24300  metrest  24420  nrginvrcn  24596  nmoge0  24625  nmoleub  24635  fsumcn  24775  cmetcaulem  25203  iscmet3  25208  iscmet2  25209  bcthlem2  25240  ovolicc2lem3  25435  itg2seq  25659  itg2splitlem  25665  itgeq1f  25688  itgeq2  25694  iblcnlem  25705  itgfsum  25743  limcnlp  25794  perfdvf  25819  dvnres  25848  dvmptfsum  25894  c1lip1  25917  dvply2g  26206  taylply2  26289  abelth  26365  cxpsqrtth  26651  rlimcnp  26884  xrlimcnp  26887  jensen  26908  ppiublem1  27122  dchrelbas3  27158  bcmono  27197  zabsle1  27216  gausslemma2dlem0f  27281  gausslemma2dlem1a  27285  gausslemma2dlem4  27289  lgsquad2lem2  27305  2lgslem1a1  27309  2lgslem3  27324  2lgs  27327  2lgsoddprm  27336  2sqlem10  27348  2sqnn  27359  addsqnreup  27363  2sqreultblem  27368  2sqreunnltblem  27371  pntrsumbnd2  27487  pntpbnd1  27506  pntlem3  27529  nolesgn2o  27591  noetalem1  27661  bday0b  27750  leftf  27779  rightf  27780  addscutlem  27881  negscut  27938  mulscutlem  28018  axcontlem7  28768  elntg2  28783  ausgrusgrb  28965  usgredg2v  29027  lfuhgr1v0e  29054  subumgredg2  29085  upgrreslem  29104  umgrreslem  29105  fusgrfisbase  29128  nbuhgr  29143  uhgrnbgr0nb  29154  nbgr0vtxlem  29155  nbgr1vtx  29158  cusgredg  29224  cusgrsizeinds  29253  sizusglecusg  29264  finsumvtxdg2size  29351  ewlkle  29406  upgriswlk  29442  pthdivtx  29530  usgr2trlncl  29561  crctcshwlkn0lem4  29611  wwlksn  29635  iswwlksnon  29651  iswspthsnon  29654  wwlksm1edg  29679  wwlksnfi  29704  2pthdlem1  29728  umgr2wlk  29747  umgrclwwlkge2  29788  clwlkclwwlklem2a  29795  clwlkclwwlk  29799  clwlkclwwlkf1lem2  29802  clwlkclwwlkf  29805  clwwisshclwws  29812  clwwlknlbonbgr1  29836  clwwlknon0  29890  clwwlknonel  29892  clwwlknonex2e  29907  3pthdlem1  29961  eupth2  30036  nfrgr2v  30069  frgr3vlem1  30070  1to2vfriswmgr  30076  1to3vfriswmgr  30077  vdgn1frgrv2  30093  frgrncvvdeqlem9  30104  frgrwopreglem4a  30107  frgrregorufr0  30121  frgrregorufr  30122  2wspmdisj  30134  2clwwlk2clwwlklem  30143  frgrreggt1  30190  frgrreg  30191  frgrregord13  30193  aevdemo  30257  shsvs  31120  0cnop  31776  0cnfn  31777  cnlnssadj  31877  ssmd1  32108  ssmd2  32109  atexch  32178  mdsymlem4  32203  sumdmdlem  32215  ifeqeqx  32318  fmptcof2  32426  padct  32485  nnindf  32564  drng0mxidl  33125  pwsiga  33685  pwldsys  33712  ldsysgenld  33715  fiunelros  33729  breprexp  34201  bnj151  34444  bnj594  34479  bnj600  34486  subfacp1lem6  34731  erdszelem8  34744  cvmliftlem7  34837  cvmliftlem10  34840  cvmlift2lem12  34860  sat1el2xp  34925  mrsubfval  35054  msubfval  35070  mclsssvlem  35108  funpartfv  35477  endofsegid  35617  broutsideof2  35654  a1i24  35721  nn0prpwlem  35742  nn0prpw  35743  ordcmp  35867  findreccl  35873  bj-ax6e  36080  bj-ax12v3ALT  36099  bj-xpnzex  36374  bj-ideqg1  36579  rdgssun  36793  finxp00  36817  domalom  36819  isinf2  36820  fvineqsneq  36827  wl-spae  36924  wl-nfs1t  36940  poimirlem27  37055  ovoliunnfl  37070  voliunnfl  37072  volsupnfl  37073  itg2addnclem3  37081  itg2addnc  37082  ftc1anc  37109  areacirclem1  37116  sdclem2  37150  fdc  37153  mettrifi  37165  isexid2  37263  zerdivemp1x  37355  smprngopr  37460  mpobi123f  37570  mptbi12f  37574  ac6s6  37580  relcnveq3  37729  mopickr  37771  elrelscnveq3  37900  disjlem14  38207  jca3  38265  ax12fromc15  38314  hbequid  38318  dvelimf-o  38338  ax12eq  38350  ax12el  38351  ax12indalem  38354  ax12inda2ALT  38355  ax12inda2  38356  lfl1dim  38530  lfl1dim2N  38531  lkreqN  38579  cvrexchlem  38829  ps-2  38888  paddasslem14  39243  idldil  39524  isltrn2N  39530  cdleme25a  39763  dibglbN  40576  dihlsscpre  40644  dvh4dimlem  40853  lcfl7N  40911  mapdval2N  41040  dvrelog2b  41474  aks6d1c6lem3  41576  nn0rppwr  41815  monotoddzzfi  42285  onov0suclim  42626  onmcl  42683  omabs2  42684  tfsconcat0b  42698  naddgeoa  42747  rp-fakeimass  42865  clublem  42963  grur1cld  43592  ee121  43867  ee122  43868  rspsbc2  43896  ax6e2ndeq  43921  vd12  43962  vd13  43963  ee221  44012  ee212  44014  ee112  44017  ee211  44020  ee210  44022  ee201  44024  ee120  44026  ee021  44028  ee012  44030  ee102  44032  ee03  44103  ee31  44114  ee31an  44116  ee123  44125  ax6e2ndeqVD  44271  ax6e2ndeqALT  44293  refsum2cnlem1  44322  fiiuncl  44352  eliin2f  44393  disjrnmpt2  44484  disjinfi  44488  rnmptbdlem  44554  allbutfi  44698  infxrunb3rnmpt  44733  infrpgernmpt  44770  monoordxrv  44787  mccl  44909  constlimc  44935  limclner  44962  xlimmnfvlem1  45143  xlimpnfvlem1  45147  ioodvbdlimc1lem2  45243  ioodvbdlimc2lem  45245  dvmptfprod  45256  dvnprodlem3  45259  stoweidlem31  45342  pwsal  45626  prsal  45629  sge0pnffigt  45707  sge0ltfirp  45711  0ome  45840  hoicvrrex  45867  hoidmvle  45911  ovnhoilem1  45912  ovnlecvr2  45921  smflimlem3  46084  funressnfv  46348  euoreqb  46412  ndmaovass  46509  afv2orxorb  46531  otiunsndisjX  46582  nltle2tri  46616  fzoopth  46630  smonoord  46634  iccpartigtl  46686  icceuelpartlem  46698  iccpartnel  46701  sprsymrelfolem2  46756  prproropf1olem4  46769  paireqne  46774  reupr  46785  reuopreuprim  46789  fmtnoprmfac1  46828  fmtnoprmfac2  46830  prmdvdsfmtnof1lem2  46848  31prm  46860  lighneallem3  46870  lighneallem4b  46872  lighneallem4  46873  lighneal  46874  nn0o1gt2ALTV  46957  nn0oALTV  46959  odd2prm2  46981  even3prm2  46982  fpprwppr  47002  stgoldbwt  47039  sbgoldbwt  47040  sbgoldbalt  47044  sbgoldbo  47050  nnsum3primesgbe  47055  wtgoldbnnsum4prm  47065  bgoldbnnsum3prm  47067  bgoldbtbndlem2  47069  bgoldbtbndlem3  47070  bgoldbtbndlem4  47071  bgoldbtbnd  47072  bgoldbachlt  47076  tgblthelfgott  47078  grimco  47101  upgrwlkupwlk  47125  rngccatidALTV  47257  ringccatidALTV  47291  lincdifsn  47415  lindslinindimp2lem1  47449  lindsrng01  47459  ldepsnlinc  47499  m1modmmod  47517  blen1b  47584  nn0sumshdiglemB  47616  nn0sumshdiglem1  47617  reorelicc  47706  rrx2xpref1o  47714  rrx2plord2  47718  rrxlinesc  47731  line2ylem  47747  line2xlem  47749  thincmon  47963  thincepi  47964