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  631  anbi1d  632  pm3.4  810  impsingle  1629  meredith  1643  stdpc4  2074  ax12  2428  ax12vALT  2474  nfsb4t  2504  moexexlem  2627  pm2.61da3ne  3022  ralrimivw  3134  rexlimdvw  3144  reximdv  3153  vtocl2d  3521  reuind  3713  reuan  3848  2reu4  4479  rabeqsnd  4628  tppreqb  4763  ssprsseq  4783  n0snor2el  4791  prnebg  4814  prel12g  4822  elpreqprlem  4824  3elpr2eq  4864  disjord  5089  disjiund  5091  dtruALT2  5317  exneq  5392  propssopi  5464  opthhausdorff  5473  fr0  5610  ssrel2  5742  poltletr  6097  reuop  6259  ordsssuc2  6418  ordnbtwn  6420  ndmfv  6874  fveqres  6886  fmptco  7084  funsndifnop  7106  tpres  7157  fntpb  7165  elunirn  7207  isof1oopb  7281  ndmovord  7558  ordsucelsuc  7774  tfinds  7812  tfindsg  7813  limomss  7823  findsg  7849  finds1  7851  xpexr  7870  resf1extb  7886  bropopvvv  8042  bropfvvvvlem  8043  bropfvvvv  8044  soxp  8081  poseq  8110  suppun  8136  extmptsuppeq  8140  funsssuppss  8142  suppss  8146  suppss2  8152  suppssfv  8154  suppco  8158  mpoxopynvov0  8170  smofvon2  8298  oaordi  8483  oawordeulem  8491  odi  8516  omeulem1  8519  brdomg  8907  snmapen  8987  fopwdom  9025  fodomr  9068  mapxpen  9083  infensuc  9095  fineqvlem  9178  fineqv  9179  fodomfir  9240  finsschain  9271  fsuppun  9302  fsuppunbi  9304  funsnfsupp  9307  dffi3  9346  fisup2g  9384  fisupcl  9385  fiinf2g  9417  infsupprpr  9421  wemapso2  9470  epnsym  9530  en3lplem2  9534  preleqg  9536  inf3lemd  9548  r1ordg  9702  r1val1  9710  r1pw  9769  r1pwALT  9770  rankxplim3  9805  eldju2ndl  9848  eldju2ndr  9849  carddomi2  9894  fidomtri  9917  alephon  9991  alephcard  9992  alephnbtwn  9993  alephordi  9996  iunfictbso  10036  fin23lem30  10264  fin1a2lem10  10331  axdc3lem2  10373  axdc3lem4  10375  alephval2  10495  cfpwsdom  10507  axextnd  10514  axrepnd  10517  axpownd  10524  axregnd  10527  axinfndlem1  10528  fpwwe2lem11  10564  wunfi  10644  addnidpi  10824  pinq  10850  mulgt0sr  11028  dedekind  11308  nnind  12175  nn1m1nn  12178  nn0n0n1ge2b  12482  nn0lt2  12567  nn0le2is012  12568  uzm1  12797  uzinfi  12853  nn01to3  12866  xrltnsym  13063  xrlttri  13065  xrlttr  13066  qbtwnxr  13127  xltnegi  13143  xnn0xaddcl  13162  xlt2add  13187  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  reltxrnmnf  13270  fzdif1  13533  fzospliti  13619  elfzonlteqm1  13669  fzoopth  13690  elfznelfzo  13701  injresinjlem  13718  injresinj  13719  modfzo0difsn  13878  addmodlteq  13881  ssnn0fi  13920  fsuppmapnn0fiub0  13928  suppssfz  13929  seqfveq2  13959  monoord  13967  seqf1o  13978  seqhomo  13984  expnngt1  14176  faclbnd4lem4  14231  hasheqf1oi  14286  hashrabsn1  14309  hashgt0elex  14336  hash1snb  14354  hashf1lem2  14391  hashf1  14392  seqcoll  14399  hashle2pr  14412  pr2pwpr  14414  hashge2el2difr  14416  swrdnnn0nd  14592  swrdnd0  14593  pfxnd0  14624  swrdswrd  14640  pfxccatin12lem3  14667  pfxccat3  14669  swrdccat3blem  14674  repsdf2  14713  repswsymballbi  14715  cshw0  14729  cshwmodn  14730  cshwn  14732  cshwcl  14733  cshwlen  14734  cshw1  14757  2cshwcshw  14760  cshimadifsn  14764  s3sndisj  14902  s3iunsndisj  14903  relexprelg  14973  relexpnndm  14976  relexpaddg  14988  relexpaddd  14989  rtrclreclem4  14996  relexpindlem  14998  rexuz3  15284  rexanuz2  15285  limsupgre  15416  rlimconst  15479  caurcvg  15612  caucvg  15614  sumss  15659  fsumcl2lem  15666  modfsummods  15728  fsumrlim  15746  fsumo1  15747  fprodcl2lem  15885  dvdsaddre2b  16246  dvdsabseq  16252  mod2eq1n2dvds  16286  nno  16321  sumeven  16326  sumodd  16327  nn0rppwr  16500  nn0seqcvgd  16509  lcmdvds  16547  lcmfunsnlem2  16579  lcmfunsnlem  16580  divgcdcoprm0  16604  ge2nprmge4  16640  exprmfct  16643  rpexp1i  16662  prm23lt5  16754  prm23ge5  16755  pcz  16821  pcadd  16829  pcmptcl  16831  oddprmdvds  16843  prmgaplem6  16996  prmgaplem7  16997  cshwshashlem1  17035  cshwsdisj  17038  prmlem0  17045  setsstruct  17115  ressress  17186  initoeu2lem2  17951  mgm2nsgrplem2  18856  mgm2nsgrplem3  18857  dfgrp2e  18905  dfgrp3e  18982  cyccom  19144  symgextf1  19362  gsmsymgrfix  19369  gsmsymgreq  19373  sylow1lem1  19539  efgsf  19670  efgrelexlema  19690  dprdss  19972  ablfac1eulem  20015  01eq0ringOLD  20476  nrhmzr  20482  funcrngcsetcALT  20586  lssssr  20917  psgnodpm  21555  psrvscafval  21916  mplcoe1  22004  mplcoe5  22007  mpfrcl  22052  mamudm  22351  matmulcell  22401  dmatmul  22453  scmatsgrp1  22478  mavmuldm  22506  mavmulsolcl  22507  mdetunilem9  22576  cramerlem3  22645  cramer0  22646  chpscmatgsumbin  22800  chp0mat  22802  fvmptnn04ifc  22808  fvmptnn04ifd  22809  epttop  22965  neiptopnei  23088  fiuncmp  23360  1stcrest  23409  kgenss  23499  hmeofval  23714  fbun  23796  fgss2  23830  filuni  23841  filssufilg  23867  filufint  23876  hausflimi  23936  hausflim  23937  hauspwpwf1  23943  fclscmp  23986  alexsubALTlem4  24006  ptcmplem3  24010  ptcmplem5  24012  cstucnd  24239  isxmet2d  24283  imasdsf1olem  24329  blfps  24362  blf  24363  metrest  24480  nrginvrcn  24648  nmoge0  24677  nmoleub  24687  fsumcn  24829  cmetcaulem  25256  iscmet3  25261  iscmet2  25262  bcthlem2  25293  ovolicc2lem3  25488  itg2seq  25711  itg2splitlem  25717  itgeq1fOLD  25741  itgeq2  25747  iblcnlem  25758  itgfsum  25796  limcnlp  25847  perfdvf  25872  dvnres  25901  dvmptfsum  25947  c1lip1  25970  dvply2g  26260  taylply2  26343  abelth  26419  cxpsqrtth  26707  rlimcnp  26943  xrlimcnp  26946  jensen  26967  ppiublem1  27181  dchrelbas3  27217  bcmono  27256  zabsle1  27275  gausslemma2dlem0f  27340  gausslemma2dlem1a  27344  gausslemma2dlem4  27348  lgsquad2lem2  27364  2lgslem1a1  27368  2lgslem3  27383  2lgs  27386  2lgsoddprm  27395  2sqlem10  27407  2sqnn  27418  addsqnreup  27422  2sqreultblem  27427  2sqreunnltblem  27430  pntrsumbnd2  27546  pntpbnd1  27565  pntlem3  27588  nolesgn2o  27651  noetalem1  27721  bday0b  27821  leftf  27863  rightf  27864  oldss  27878  addcutslem  27985  negcut  28047  mulcutlem  28139  n0s0suc  28350  n0fincut  28363  n0s0m1  28370  nn1m1nns  28382  axcontlem7  29055  elntg2  29070  ausgrusgrb  29250  usgredg2v  29312  lfuhgr1v0e  29339  subumgredg2  29370  upgrreslem  29389  umgrreslem  29390  fusgrfisbase  29413  nbuhgr  29428  uhgrnbgr0nb  29439  nbgr0edglem  29441  nbgr1vtx  29443  cusgredg  29509  cusgrsizeinds  29538  sizusglecusg  29549  finsumvtxdg2size  29636  ewlkle  29691  upgriswlk  29726  pthdivtx  29812  dfpth2  29814  usgr2trlncl  29845  crctcshwlkn0lem4  29898  wwlksn  29922  iswwlksnon  29938  iswspthsnon  29941  wwlksm1edg  29966  wwlksnfi  29991  2pthdlem1  30015  umgr2wlk  30034  umgrclwwlkge2  30078  clwlkclwwlklem2a  30085  clwlkclwwlk  30089  clwlkclwwlkf1lem2  30092  clwlkclwwlkf  30095  clwwisshclwws  30102  clwwlknlbonbgr1  30126  clwwlknon0  30180  clwwlknonel  30182  clwwlknonex2e  30197  3pthdlem1  30251  eupth2  30326  nfrgr2v  30359  frgr3vlem1  30360  1to2vfriswmgr  30366  1to3vfriswmgr  30367  vdgn1frgrv2  30383  frgrncvvdeqlem9  30394  frgrwopreglem4a  30397  frgrregorufr0  30411  frgrregorufr  30412  2wspmdisj  30424  2clwwlk2clwwlklem  30433  frgrreggt1  30480  frgrreg  30481  frgrregord13  30483  aevdemo  30547  shsvs  31410  0cnop  32066  0cnfn  32067  cnlnssadj  32167  ssmd1  32398  ssmd2  32399  atexch  32468  mdsymlem4  32493  sumdmdlem  32505  ifeqeqx  32628  fmptcof2  32746  padct  32807  nnindf  32910  drng0mxidl  33568  constr01  33919  pwsiga  34307  pwldsys  34334  ldsysgenld  34337  fiunelros  34351  breprexp  34810  bnj151  35052  bnj594  35087  bnj600  35094  trssfir1om  35286  trssfir1omregs  35311  subfacp1lem6  35398  erdszelem8  35411  cvmliftlem7  35504  cvmliftlem10  35507  cvmlift2lem12  35527  sat1el2xp  35592  mrsubfval  35721  msubfval  35737  mclsssvlem  35775  antnestlaw2  35905  funpartfv  36158  endofsegid  36298  broutsideof2  36335  a1i24  36514  nn0prpwlem  36535  nn0prpw  36536  ordcmp  36660  findreccl  36666  bj-cbvaw  36878  bj-cbveaw  36880  bj-ax6e  36907  bj-ax12v3ALT  36925  bj-xpnzex  37201  bj-ideqg1  37413  rdgssun  37627  finxp00  37651  domalom  37653  isinf2  37654  fvineqsneq  37661  wl-spae  37770  wl-nfs1t  37786  poimirlem27  37892  ovoliunnfl  37907  voliunnfl  37909  volsupnfl  37910  itg2addnclem3  37918  itg2addnc  37919  ftc1anc  37946  areacirclem1  37953  sdclem2  37987  fdc  37990  mettrifi  38002  isexid2  38100  zerdivemp1x  38192  smprngopr  38297  mpobi123f  38407  mptbi12f  38411  ac6s6  38417  relcnveq3  38572  mopickr  38616  elrelscnveq3  38872  disjlem14  39146  jca3  39226  ax12fromc15  39275  hbequid  39279  dvelimf-o  39299  ax12eq  39311  ax12el  39312  ax12indalem  39315  ax12inda2ALT  39316  ax12inda2  39317  lfl1dim  39491  lfl1dim2N  39492  lkreqN  39540  cvrexchlem  39789  ps-2  39848  paddasslem14  40203  idldil  40484  isltrn2N  40490  cdleme25a  40723  dibglbN  41536  dihlsscpre  41604  dvh4dimlem  41813  lcfl7N  41871  mapdval2N  42000  dvrelog2b  42430  aks6d1c6lem3  42536  monotoddzzfi  43293  onov0suclim  43625  onmcl  43682  omabs2  43683  tfsconcat0b  43697  naddgeoa  43745  rp-fakeimass  43862  clublem  43960  grur1cld  44582  ee121  44855  ee122  44856  rspsbc2  44884  ax6e2ndeq  44909  vd12  44950  vd13  44951  ee221  45000  ee212  45002  ee112  45005  ee211  45008  ee210  45010  ee201  45012  ee120  45014  ee021  45016  ee012  45018  ee102  45020  ee03  45090  ee31  45101  ee31an  45103  ee123  45112  ax6e2ndeqVD  45258  ax6e2ndeqALT  45280  refsum2cnlem1  45391  fiiuncl  45419  eliin2f  45457  disjrnmpt2  45541  disjinfi  45545  rnmptbdlem  45607  allbutfi  45745  infxrunb3rnmpt  45780  infrpgernmpt  45817  monoordxrv  45833  mccl  45952  constlimc  45978  limclner  46003  xlimmnfvlem1  46184  xlimpnfvlem1  46188  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvnprodlem3  46300  stoweidlem31  46383  pwsal  46667  prsal  46670  sge0pnffigt  46748  sge0ltfirp  46752  0ome  46881  hoicvrrex  46908  hoidmvle  46952  ovnhoilem1  46953  ovnlecvr2  46962  smflimlem3  47125  ormkglobd  47227  chnsubseqword  47230  funressnfv  47397  euoreqb  47463  ndmaovass  47560  afv2orxorb  47582  otiunsndisjX  47633  nltle2tri  47667  m1modmmod  47712  smonoord  47725  iccpartigtl  47777  icceuelpartlem  47789  iccpartnel  47792  sprsymrelfolem2  47847  prproropf1olem4  47860  paireqne  47865  reupr  47876  reuopreuprim  47880  fmtnoprmfac1  47919  fmtnoprmfac2  47921  prmdvdsfmtnof1lem2  47939  31prm  47951  lighneallem3  47961  lighneallem4b  47963  lighneallem4  47964  lighneal  47965  nn0o1gt2ALTV  48048  nn0oALTV  48050  odd2prm2  48072  even3prm2  48073  fpprwppr  48093  stgoldbwt  48130  sbgoldbwt  48131  sbgoldbalt  48135  sbgoldbo  48141  nnsum3primesgbe  48146  wtgoldbnnsum4prm  48156  bgoldbnnsum3prm  48158  bgoldbtbndlem2  48160  bgoldbtbndlem3  48161  bgoldbtbndlem4  48162  bgoldbtbnd  48163  bgoldbachlt  48167  tgblthelfgott  48169  dfclnbgr6  48210  grimco  48243  uhgrimisgrgric  48285  grtriprop  48295  usgrgrtrirex  48304  isubgr3stgrlem6  48325  isubgr3stgrlem8  48327  grlimprclnbgr  48350  grlimgrtri  48357  gpgedg2ov  48420  gpg5nbgrvtx03starlem1  48422  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx03starlem3  48424  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem2  48426  gpg5nbgrvtx13starlem3  48427  gpgcubic  48433  gpg5nbgr3star  48435  gpgprismgr4cycllem7  48455  pgnbgreunbgrlem2  48471  gpg5edgnedg  48484  upgrwlkupwlk  48494  rngccatidALTV  48626  ringccatidALTV  48660  lincdifsn  48778  lindslinindimp2lem1  48812  lindsrng01  48822  ldepsnlinc  48862  blen1b  48942  nn0sumshdiglemB  48974  nn0sumshdiglem1  48975  reorelicc  49064  rrx2xpref1o  49072  rrx2plord2  49076  rrxlinesc  49089  line2ylem  49105  line2xlem  49107  thincmon  49786  thincepi  49787