Theorem a1d 26

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 18	1 ⊢ (𝜑 → (𝜒 → 𝜓))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  2a1d  27  a1i13  28  syl5com  32  mpid  45  syld  48  imim2d  58  syl6ci  72  syl5d  74  syl6d  76  pm2.21d  122  pm2.24d  152  conax1k  172  pm2.521g2  176  pm2.61iii  187  mtod  201  imbi2d  343  adantr  486  jctild  535  jctird  536  anbi2d  642  anbi1d  643  pm3.4  822  impsingle  1660  meredith  1674  stdpc4  2105  ax12  2453  ax12vALT  2499  nfsb4t  2529  moexexlem  2652  pm2.61da3ne  3045  ralrimivw  3159  rexlimdvw  3169  reximdv  3178  vtocl2d  3524  reuind  3711  reuan  3844  2reu4  4480  rabeqsnd  4630  tppreqb  4768  ssprsseq  4786  n0snor2el  4793  prnebg  4816  prel12g  4824  elpreqprlem  4826  3elpr2eq  4866  disjord  5092  disjiund  5094  dtruALT2  5332  exneq  5404  propssopi  5480  opthhausdorff  5490  fr0  5629  ssrel2  5761  poltletr  6124  reuop  6289  ordsssuc2  6449  ordnbtwn  6451  ndmfv  6909  fveqres  6921  fmptco  7122  funsndifnop  7147  tpres  7199  fntpb  7207  elunirn  7247  isof1oopb  7325  ndmovord  7603  ordsucelsuc  7822  tfinds  7860  tfindsg  7861  limomss  7871  findsg  7898  finds1  7900  xpexr  7919  resf1extb  7935  bropopvvv  8090  bropfvvvvlem  8091  bropfvvvv  8092  soxp  8130  poseq  8159  suppun  8185  extmptsuppeq  8189  funsssuppss  8191  suppss  8195  suppss2  8201  suppssfv  8203  suppco  8207  mpoxopynvov0  8219  smofvon2  8348  oaordi  8538  oawordeulem  8546  odi  8571  omeulem1  8574  brdomg  8969  snmapen  9050  fopwdom  9088  fodomr  9131  mapxpen  9146  infensuc  9158  fineqvlem  9241  fineqv  9242  fodomfir  9303  finsschain  9332  fsuppun  9363  fsuppunbi  9365  funsnfsupp  9368  dffi3  9407  fisup2g  9445  fisupcl  9446  fiinf2g  9478  infsupprpr  9482  wemapso2  9531  epnsym  9594  en3lplem2  9598  preleqg  9600  inf3lemd  9612  r1ordg  9768  r1val1  9776  r1pw  9840  r1pwALT  9841  rankxplim3  9879  eldju2ndl  9986  eldju2ndr  9987  carddomi2  10032  fidomtri  10055  alephon  10129  alephcard  10130  alephnbtwn  10131  alephordi  10134  iunfictbso  10174  fin23lem30  10401  fin1a2lem10  10468  axdc3lem2  10510  axdc3lem4  10512  alephval2  10638  cfpwsdom  10650  axextnd  10657  axrepnd  10660  axpownd  10667  axregnd  10670  axinfndlem1  10671  fpwwe2lem11  10707  wunfi  10787  addnidpi  10967  pinq  10993  mulgt0sr  11171  dedekind  11454  indval0  12305  nnind  12334  nn1m1nn  12337  nn0n0n1ge2b  12656  nn0lt2  12743  nn0le2is012  12744  uzm1  12980  uzinfi  13036  nn01to3  13049  xrltnsym  13247  xrlttri  13249  xrlttr  13250  qbtwnxr  13311  xltnegi  13327  xnn0xaddcl  13346  xlt2add  13371  xrsupsslem  13418  xrinfmsslem  13419  xrub  13423  reltxrnmnf  13454  fzdif1  13719  fzospliti  13806  elfzonlteqm1  13856  fzoopth  13877  elfznelfzo  13888  injresinjlem  13905  injresinj  13906  modfzo0difsn  14066  addmodlteq  14069  ssnn0fi  14108  fsuppmapnn0fiub0  14116  suppssfz  14117  seqfveq2  14147  monoord  14155  seqf1o  14166  seqhomo  14172  expnngt1  14365  faclbnd4lem4  14420  hasheqf1oi  14475  hashrabsn1  14498  hashgt0elex  14525  hash1snb  14544  hashf1lem2  14581  hashf1  14582  seqcoll  14589  hashle2pr  14602  pr2pwpr  14604  hashge2el2difr  14606  swrdnnn0nd  14786  swrdnd0  14787  pfxnd0  14818  swrdswrd  14834  pfxccatin12lem3  14861  pfxccat3  14863  swrdccat3blem  14868  repsdf2  14909  repswsymballbi  14911  cshw0  14925  cshwmodn  14926  cshwn  14928  cshwcl  14929  cshwlen  14930  cshw1  14953  2cshwcshw  14956  cshimadifsn  14960  s3sndisj  15100  s3iunsndisj  15101  relexprelg  15171  relexpnndm  15174  relexpaddg  15186  relexpaddd  15187  rtrclreclem4  15194  relexpindlem  15196  rexuz3  15496  rexanuz2  15497  limsupgre  15628  rlimconst  15691  caurcvg  15824  caucvg  15826  sumss  15870  fsumcl2lem  15877  modfsummods  15940  fsumrlim  15958  fsumo1  15959  fprodcl2lem  16097  dvdsaddre2b  16457  dvdsabseq  16463  mod2eq1n2dvds  16497  nno  16532  sumeven  16537  sumodd  16538  nn0rppwr  16715  nn0seqcvgd  16725  lcmdvds  16763  lcmfunsnlem2  16795  lcmfunsnlem  16796  divgcdcoprm0  16820  ge2nprmge4  16857  exprmfct  16860  rpexp1i  16879  prm23lt5  16972  prm23ge5  16973  pcz  17039  pcadd  17047  pcmptcl  17049  oddprmdvds  17061  prmgaplem6  17214  prmgaplem7  17215  cshwshashlem1  17253  cshwsdisj  17256  prmlem0  17263  setsstruct  17334  ressress  17405  initoeu2lem2  18170  mgmn0plusgf  18807  mgm2nsgrplem2  19098  mgm2nsgrplem3  19099  dfgrp2e  19154  dfgrp3e  19230  cyccom  19398  symgextf1  19615  gsmsymgrfix  19622  gsmsymgreq  19626  sylow1lem1  19792  efgsf  19923  efgrelexlema  19943  dprdss  20225  ablfac1eulem  20268  01eq0ringOLD  20762  nrhmzr  20769  funcrngcsetcALT  20873  lssssr  21209  isfieldidl  21520  psgnodpm  21874  psrvscafval  22236  mplcoe1  22326  mplcoe5  22329  mpfrcl  22374  mamudm  22690  matmulcell  22740  dmatmul  22792  scmatsgrp1  22817  mavmuldm  22845  mavmulsolcl  22846  mdetunilem9  22915  cramerlem3  22987  cramer0  22988  chpscmatgsumbin  23142  chp0mat  23144  fvmptnn04ifc  23150  fvmptnn04ifd  23151  epttop  23307  neiptopnei  23430  fiuncmp  23702  1stcrest  23751  kgenss  23842  hmeofval  24057  fbun  24139  fgss2  24173  filuni  24184  filssufilg  24210  filufint  24219  hausflimi  24279  hausflim  24280  hauspwpwf1  24286  fclscmp  24329  alexsubALTlem4  24349  ptcmplem3  24353  ptcmplem5  24355  cstucnd  24582  isxmet2d  24626  imasdsf1olem  24672  blfps  24705  blf  24706  metrest  24823  nrginvrcn  24991  nmoge0  25020  nmoleub  25030  fsumcn  25171  cmetcaulem  25589  iscmet3  25594  iscmet2  25595  bcthlem2  25626  ovolicc2lem3  25820  itg2seq  26043  itg2splitlem  26049  itgeq2  26078  iblcnlem  26089  itgfsum  26127  limcnlp  26178  perfdvf  26203  dvnres  26231  dvmptfsum  26275  c1lip1  26297  dvply2g  26588  taylply2  26677  abelth  26750  cxpsqrtth  27040  rlimcnp  27275  xrlimcnp  27278  jensen  27298  ppiublem1  27511  dchrelbas3  27547  bcmono  27586  zabsle1  27605  gausslemma2dlem0f  27670  gausslemma2dlem1a  27674  gausslemma2dlem4  27678  lgsquad2lem2  27694  2lgslem1a1  27698  2lgslem3  27713  2lgs  27716  2lgsoddprm  27725  2sqlem10  27737  2sqnn  27748  addsqnreup  27752  2sqreultblem  27757  2sqreunnltblem  27760  pntrsumbnd2  27876  pntpbnd1  27895  pntlem3  27918  fltoprmgt3  27978  nolesgn2o  28010  noetalem1  28080  bday0b  28181  leftf  28223  rightf  28224  oldss  28238  addcutslem  28345  negcut  28407  mulcutlem  28499  n0s0suc  28710  n0fincut  28723  n0s0m1  28730  nn1m1nns  28742  axcontlem7  29530  elntg2  29545  ausgrusgrb  29728  usgredg2v  29790  lfuhgr1v0e  29817  subumgredg2  29848  upgrreslem  29867  umgrreslem  29868  fusgrfisbase  29891  nbuhgr  29906  uhgrnbgr0nb  29917  nbgr0edglem  29919  nbgr1vtx  29921  cusgredg  29987  cusgrsizeinds  30015  sizusglecusg  30026  finsumvtxdg2size  30113  ewlkle  30168  upgriswlk  30203  pthdivtx  30294  dfpth2  30296  usgr2trlncl  30328  crctcshwlkn0lem4  30384  wwlksn  30408  iswwlksnon  30424  iswspthsnon  30427  wwlksm1edg  30452  wwlksnfi  30477  2pthdlem1  30501  umgr2wlk  30520  umgrclwwlkge2  30564  clwlkclwwlklem2a  30571  clwlkclwwlk  30575  clwlkclwwlkf1lem2  30578  clwlkclwwlkf  30581  clwwisshclwws  30588  clwwlknlbonbgr1  30612  clwwlknon0  30666  clwwlknonel  30668  clwwlknonex2e  30683  3pthdlem1  30747  eupth2  30822  nfrgr2v  30855  frgr3vlem1  30856  1to2vfriswmgr  30862  1to3vfriswmgr  30863  vdgn1frgrv2  30879  frgrncvvdeqlem9  30890  frgrwopreglem4a  30893  frgrregorufr0  30907  frgrregorufr  30908  2wspmdisj  30920  2clwwlk2clwwlklem  30929  frgrreggt1  30976  frgrreg  30977  frgrregord13  30979  aevdemo  31043  shsvs  31907  0cnop  32563  0cnfn  32564  cnlnssadj  32664  ssmd1  32895  ssmd2  32896  atexch  32965  mdsymlem4  32990  sumdmdlem  33002  ifeqeqx  33120  fmptcof2  33233  padct  33292  nnindf  33393  drng0mxidl  33982  constr01  34356  pwsiga  34744  pwldsys  34772  ldsysgenld  34775  fiunelros  34789  breprexp  35245  bnj151  35490  bnj594  35525  bnj600  35532  trssfir1om  35716  rankscottu  35731  trssfir1omregs  35777  subfacp1lem6  35919  erdszelem8  35932  cvmliftlem7  36025  cvmliftlem10  36028  cvmlift2lem12  36048  sat1el2xp  36113  mrsubfval  36242  msubfval  36258  mclsssvlem  36296  antnestlaw2  36426  funpartfv  36679  endofsegid  36820  broutsideof2  36857  a1i24  37060  nn0prpwlem  37080  nn0prpw  37081  ordcmp  37205  findreccl  37211  axtcond  37236  dfttc2g  37264  dfttc4lem2  37287  bj-cbvaw  37510  bj-cbveaw  37512  bj-ax6e  37537  bj-ax12v3ALT  37558  bj-xpnzex  37842  bj-ideqg1  38053  rdgssun  38269  finxp00  38293  domalom  38295  isinf2  38296  fvineqsneq  38303  wl-spae  38421  wl-nfs1t  38437  poimirlem27  38533  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  itg2addnclem3  38559  itg2addnc  38560  ftc1anc  38587  areacirclem1  38594  sdclem2  38644  fdc  38647  mettrifi  38659  isexid2  38757  zerdivemp1x  38849  smprngopr  38954  mpobi123f  39062  mptbi12f  39066  ac6s6  39072  relcnveq3  39227  mopickr  39271  elrelscnveq3  39527  disjlem14  39801  jca3  39881  ax12fromc15  39930  hbequid  39934  dvelimf-o  39954  ax12eq  39966  ax12el  39967  ax12indalem  39970  ax12inda2ALT  39971  ax12inda2  39972  lfl1dim  40146  lfl1dim2N  40147  lkreqN  40195  cvrexchlem  40444  ps-2  40503  paddasslem14  40858  idldil  41139  isltrn2N  41145  cdleme25a  41378  dibglbN  42191  dihlsscpre  42259  dvh4dimlem  42468  lcfl7N  42526  mapdval2N  42655  dvrelog2b  43084  aks6d1c6lem3  43190  monotoddzzfi  43902  onov0suclim  44234  onmcl  44291  omabs2  44292  tfsconcat0b  44306  naddgeoa  44354  rp-fakeimass  44471  clublem  44569  grur1cld  45189  ee121  45447  ee122  45448  rspsbc2  45476  ax6e2ndeq  45501  vd12  45542  vd13  45543  ee221  45592  ee212  45594  ee112  45597  ee211  45600  ee210  45602  ee201  45604  ee120  45606  ee021  45608  ee012  45610  ee102  45612  ee03  45682  ee31  45693  ee31an  45695  ee123  45704  ax6e2ndeqVD  45850  ax6e2ndeqALT  45872  refsum2cnlem1  45997  fiiuncl  46025  eliin2f  46062  disjrnmpt2  46146  disjinfi  46150  rnmptbdlem  46210  allbutfi  46348  infxrunb3rnmpt  46382  infrpgernmpt  46419  monoordxrv  46435  mccl  46554  constlimc  46580  limclner  46605  xlimmnfvlem1  46786  xlimpnfvlem1  46790  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvnprodlem3  46902  stoweidlem31  46985  pwsal  47269  prsal  47272  sge0pnffigt  47350  sge0ltfirp  47354  0ome  47483  hoicvrrex  47510  hoidmvle  47554  ovnhoilem1  47555  ovnlecvr2  47564  smflimlem3  47727  ormkglobd  47831  tmachlem-agreeprod  47891  funressnfv  48057  euoreqb  48123  ndmaovass  48220  afv2orxorb  48242  otiunsndisjX  48293  nltle2tri  48327  nnmul2b  48345  m1modmmod  48378  smonoord  48391  iccpartigtl  48449  icceuelpartlem  48461  iccpartnel  48464  sprsymrelfolem2  48519  prproropf1olem4  48532  paireqne  48537  reupr  48548  reuopreuprim  48552  nprmmul3  48555  fmtnoprmfac1  48594  fmtnoprmfac2  48596  prmdvdsfmtnof1lem2  48614  31prm  48626  lighneallem3  48636  lighneallem4b  48638  lighneallem4  48639  lighneal  48640  nprmdvdsfacm1lem2  48650  ppivalnnnprm  48657  nn0o1gt2ALTV  48736  nn0oALTV  48738  odd2prm2  48760  even3prm2  48761  fpprwppr  48781  stgoldbwt  48818  sbgoldbwt  48819  sbgoldbalt  48823  sbgoldbo  48829  nnsum3primesgbe  48834  wtgoldbnnsum4prm  48844  bgoldbnnsum3prm  48846  bgoldbtbndlem2  48848  bgoldbtbndlem3  48849  bgoldbtbndlem4  48850  bgoldbtbnd  48851  bgoldbachlt  48855  tgblthelfgott  48857  dfclnbgr6  48898  grimco  48931  uhgrimisgrgric  48973  grtriprop  48983  usgrgrtrirex  48992  isubgr3stgrlem6  49013  isubgr3stgrlem8  49015  grlimprclnbgr  49038  grlimgrtri  49045  gpgedg2ov  49108  gpg5nbgrvtx03starlem1  49110  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx03starlem3  49112  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem2  49114  gpg5nbgrvtx13starlem3  49115  gpgcubic  49121  gpg5nbgr3star  49123  gpgprismgr4cycllem7  49143  pgnbgreunbgrlem2  49159  gpg5edgnedg  49172  upgrwlkupwlk  49182  rngccatidALTV  49313  ringccatidALTV  49347  lincdifsn  49480  lindslinindimp2lem1  49514  lindsrng01  49524  ldepsnlinc  49564  blen1b  49644  nn0sumshdiglemB  49676  nn0sumshdiglem1  49677  reorelicc  49766  rrx2xpref1o  49774  rrx2plord2  49778  rrxlinesc  49791  line2ylem  49807  line2xlem  49809  thincmon  50485  thincepi  50486