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  2107  ax12  2455  ax12vALT  2501  nfsb4t  2531  moexexlem  2654  pm2.61da3ne  3048  ralrimivw  3162  rexlimdvw  3172  reximdv  3181  vtocl2d  3527  reuind  3714  reuan  3848  2reu4  4483  rabeqsnd  4630  tppreqb  4768  ssprsseq  4784  n0snor2el  4791  prnebg  4814  prel12g  4822  elpreqprlem  4824  3elpr2eq  4837  disjord  5095  disjiund  5097  dtruALT2  5337  exneq  5409  propssopi  5485  opthhausdorff  5495  fr0  5634  ssrel2  5767  poltletr  6139  reuop  6317  ordsssuc2  6477  ordnbtwn  6479  ndmfv  6943  fveqres  6955  fmptco  7157  funsndifnop  7182  tpres  7233  fntpb  7241  elunirn  7281  isof1oopb  7359  ndmovord  7638  ordsucelsuc  7860  tfinds  7898  tfindsg  7899  limomss  7909  findsg  7936  finds1  7938  xpexr  7957  resf1extb  7973  bropopvvv  8129  bropfvvvvlem  8130  bropfvvvv  8131  soxp  8171  poseq  8205  suppun  8232  extmptsuppeq  8236  funsssuppss  8238  suppss  8242  suppss2  8248  suppssfv  8250  suppco  8254  mpoxopynvov0  8266  smofvon2  8395  oaordi  8585  oawordeulem  8593  odi  8618  omeulem1  8621  brdomg  9016  snmapen  9097  fopwdom  9135  fodomr  9178  mapxpen  9193  infensuc  9205  fineqvlem  9288  fineqv  9289  fodomfir  9350  finsschain  9379  fsuppun  9409  fsuppunbi  9411  funsnfsupp  9414  dffi3  9453  fisup2g  9491  fisupcl  9492  fiinf2g  9524  infsupprpr  9528  wemapso2  9577  epnsym  9640  en3lplem2  9644  preleqg  9646  inf3lemd  9658  r1ordg  9815  r1val1  9823  r1pw  9889  r1pwALT  9890  rankxplim3  9928  eldju2ndl  10035  eldju2ndr  10036  carddomi2  10081  fidomtri  10104  alephon  10178  alephcard  10179  alephnbtwn  10180  alephordi  10183  iunfictbso  10223  fin23lem30  10450  fin1a2lem10  10517  axdc3lem2  10559  axdc3lem4  10561  alephval2  10687  cfpwsdom  10699  axextnd  10706  axrepnd  10709  axpownd  10716  axregnd  10719  axinfndlem1  10720  fpwwe2lem11  10756  wunfi  10836  addnidpi  11016  pinq  11042  mulgt0sr  11220  dedekind  11503  indval0  12354  nnind  12383  nn1m1nn  12386  nn0n0n1ge2b  12705  nn0lt2  12792  nn0le2is012  12793  uzm1  13029  uzinfi  13085  nn01to3  13098  xrltnsym  13296  xrlttri  13298  xrlttr  13299  qbtwnxr  13360  xltnegi  13376  xnn0xaddcl  13395  xlt2add  13420  xrsupsslem  13467  xrinfmsslem  13468  xrub  13472  reltxrnmnf  13503  fzdif1  13769  fzospliti  13856  elfzonlteqm1  13906  fzoopth  13927  elfznelfzo  13938  injresinjlem  13955  injresinj  13956  modfzo0difsn  14116  addmodlteq  14119  ssnn0fi  14158  fsuppmapnn0fiub0  14166  suppssfz  14167  seqfveq2  14197  monoord  14205  seqf1o  14216  seqhomo  14222  expnngt1  14415  faclbnd4lem4  14470  hasheqf1oi  14525  hashrabsn1  14548  hashgt0elex  14575  hash1snb  14594  hashf1lem2  14631  hashf1  14632  seqcoll  14639  hashle2pr  14652  pr2pwpr  14654  hashge2el2difr  14656  swrdnnn0nd  14837  swrdnd0  14838  pfxnd0  14869  swrdswrd  14885  pfxccatin12lem3  14912  pfxccat3  14914  swrdccat3blem  14919  repsdf2  14960  repswsymballbi  14962  cshw0  14976  cshwmodn  14977  cshwn  14979  cshwcl  14980  cshwlen  14981  cshw1  15004  2cshwcshw  15007  cshimadifsn  15011  s3sndisj  15152  s3iunsndisj  15153  relexprelg  15223  relexpnndm  15226  relexpaddg  15238  relexpaddd  15239  rtrclreclem4  15246  relexpindlem  15248  rexuz3  15548  rexanuz2  15549  limsupgre  15680  rlimconst  15743  caurcvg  15876  caucvg  15878  sumss  15922  fsumcl2lem  15929  modfsummods  15992  fsumrlim  16010  fsumo1  16011  fprodcl2lem  16149  dvdsaddre2b  16509  dvdsabseq  16515  mod2eq1n2dvds  16549  nno  16584  sumeven  16589  sumodd  16590  nn0rppwr  16767  nn0seqcvgd  16777  lcmdvds  16815  lcmfunsnlem2  16847  lcmfunsnlem  16848  divgcdcoprm0  16872  ge2nprmge4  16909  exprmfct  16912  rpexp1i  16931  prm23lt5  17024  prm23ge5  17025  pcz  17091  pcadd  17099  pcmptcl  17101  oddprmdvds  17113  prmgaplem6  17266  prmgaplem7  17267  cshwshashlem1  17305  cshwsdisj  17308  prmlem0  17315  setsstruct  17386  ressress  17457  initoeu2lem2  18222  mgmn0plusgf  18859  mgm2nsgrplem2  19150  mgm2nsgrplem3  19151  dfgrp2e  19206  dfgrp3e  19282  cyccom  19450  symgextf1  19668  gsmsymgrfix  19675  gsmsymgreq  19679  sylow1lem1  19845  efgsf  19976  efgrelexlema  19996  dprdss  20278  ablfac1eulem  20321  01eq0ringOLD  20815  nrhmzr  20822  funcrngcsetcALT  20926  lssssr  21262  isfieldidl  21573  psgnodpm  21927  psrvscafval  22289  mplcoe1  22379  mplcoe5  22382  mpfrcl  22427  mamudm  22743  matmulcell  22793  dmatmul  22845  scmatsgrp1  22870  mavmuldm  22898  mavmulsolcl  22899  mdetunilem9  22968  cramerlem3  23040  cramer0  23041  chpscmatgsumbin  23195  chp0mat  23197  fvmptnn04ifc  23203  fvmptnn04ifd  23204  epttop  23360  neiptopnei  23483  fiuncmp  23755  1stcrest  23804  kgenss  23895  hmeofval  24110  fbun  24192  fgss2  24226  filuni  24237  filssufilg  24263  filufint  24272  hausflimi  24332  hausflim  24333  hauspwpwf1  24339  fclscmp  24382  alexsubALTlem4  24402  ptcmplem3  24406  ptcmplem5  24408  cstucnd  24635  isxmet2d  24679  imasdsf1olem  24725  blfps  24758  blf  24759  metrest  24876  nrginvrcn  25044  nmoge0  25073  nmoleub  25083  fsumcn  25224  cmetcaulem  25642  iscmet3  25647  iscmet2  25648  bcthlem2  25679  ovolicc2lem3  25873  itg2seq  26096  itg2splitlem  26102  itgeq2  26131  iblcnlem  26142  itgfsum  26180  limcnlp  26231  perfdvf  26256  dvnres  26284  dvmptfsum  26328  c1lip1  26350  dvply2g  26639  taylply2  26728  abelth  26801  cxpsqrtth  27091  rlimcnp  27326  xrlimcnp  27329  jensen  27349  ppiublem1  27562  dchrelbas3  27598  bcmono  27637  zabsle1  27656  gausslemma2dlem0f  27721  gausslemma2dlem1a  27725  gausslemma2dlem4  27729  lgsquad2lem2  27745  2lgslem1a1  27749  2lgslem3  27764  2lgs  27767  2lgsoddprm  27776  2sqlem10  27788  2sqnn  27799  addsqnreup  27803  2sqreultblem  27808  2sqreunnltblem  27811  pntrsumbnd2  27927  pntpbnd1  27946  pntlem3  27969  fltoprmgt3  28029  nolesgn2o  28061  noetalem1  28131  bday0b  28232  leftf  28274  rightf  28275  oldss  28289  addcutslem  28396  negcut  28458  mulcutlem  28550  n0s0suc  28761  n0fincut  28774  n0s0m1  28781  nn1m1nns  28793  axcontlem7  29581  elntg2  29596  ausgrusgrb  29779  usgredg2v  29841  lfuhgr1v0e  29868  subumgredg2  29899  upgrreslem  29918  umgrreslem  29919  fusgrfisbase  29942  nbuhgr  29957  uhgrnbgr0nb  29968  nbgr0edglem  29970  nbgr1vtx  29972  cusgredg  30038  cusgrsizeinds  30066  sizusglecusg  30077  finsumvtxdg2size  30164  ewlkle  30219  upgriswlk  30254  pthdivtx  30345  dfpth2  30347  usgr2trlncl  30379  crctcshwlkn0lem4  30435  wwlksn  30459  iswwlksnon  30475  iswspthsnon  30478  wwlksm1edg  30503  wwlksnfi  30528  2pthdlem1  30552  umgr2wlk  30571  umgrclwwlkge2  30615  clwlkclwwlklem2a  30622  clwlkclwwlk  30626  clwlkclwwlkf1lem2  30629  clwlkclwwlkf  30632  clwwisshclwws  30639  clwwlknlbonbgr1  30663  clwwlknon0  30717  clwwlknonel  30719  clwwlknonex2e  30734  3pthdlem1  30798  eupth2  30873  nfrgr2v  30906  frgr3vlem1  30907  1to2vfriswmgr  30913  1to3vfriswmgr  30914  vdgn1frgrv2  30930  frgrncvvdeqlem9  30941  frgrwopreglem4a  30944  frgrregorufr0  30958  frgrregorufr  30959  2wspmdisj  30971  2clwwlk2clwwlklem  30980  frgrreggt1  31027  frgrreg  31028  frgrregord13  31030  aevdemo  31094  shsvs  31958  0cnop  32614  0cnfn  32615  cnlnssadj  32715  ssmd1  32946  ssmd2  32947  atexch  33016  mdsymlem4  33041  sumdmdlem  33053  ifeqeqx  33213  fmptcof2  33326  padct  33384  nnindf  33484  drng0mxidl  34084  constr01  34457  pwsiga  34845  pwldsys  34873  ldsysgenld  34876  fiunelros  34890  breprexp  35345  bnj151  35590  bnj594  35625  bnj600  35632  rmo6  35793  soinfdom  35813  trssfihf  35832  rankscottu  35852  trssfihfregs  35917  onf1oracwevd  36065  srepdflem2  36099  subfacp1lem6  36130  erdszelem8  36143  cvmliftlem7  36236  cvmliftlem10  36239  cvmlift2lem12  36259  sat1el2xp  36324  mrsubfval  36453  msubfval  36469  mclsssvlem  36507  antnestlaw2  36637  funpartfv  36900  endofsegid  37041  broutsideof2  37078  a1i24  37281  nn0prpwlem  37301  nn0prpw  37302  ordcmp  37426  findreccl  37432  axtcond  37457  dfttc2g  37485  dfttc4lem2  37508  bj-cbvaw  37731  bj-cbveaw  37733  bj-ax6e  37758  bj-ax12v3ALT  37779  bj-xpnzex  38063  bj-ideqg1  38290  rdgssun  38506  finxp00  38530  domalom  38532  isinf2  38533  fvineqsneq  38540  wl-spae  38658  wl-nfs1t  38674  poimirlem27  38770  ovoliunnfl  38785  voliunnfl  38787  volsupnfl  38788  itg2addnclem3  38796  itg2addnc  38797  ftc1anc  38824  areacirclem1  38831  sdclem2  38879  fdc  38882  mettrifi  38894  isexid2  38992  zerdivemp1x  39084  smprngopr  39189  mpobi123f  39297  mptbi12f  39301  ac6s6  39307  relcnveq3  39462  mopickr  39506  elrelscnveq3  39762  disjlem14  40036  jca3  40116  ax12fromc15  40165  hbequid  40169  dvelimf-o  40189  ax12eq  40201  ax12el  40202  ax12indalem  40205  ax12inda2ALT  40206  ax12inda2  40207  lfl1dim  40381  lfl1dim2N  40382  lkreqN  40430  cvrexchlem  40679  ps-2  40738  paddasslem14  41093  idldil  41374  isltrn2N  41380  cdleme25a  41613  dibglbN  42426  dihlsscpre  42494  dvh4dimlem  42703  lcfl7N  42761  mapdval2N  42890  dvrelog2b  43319  aks6d1c6lem3  43425  monotoddzzfi  44153  onov0suclim  44479  onmcl  44536  omabs2  44537  tfsconcat0b  44551  naddgeoa  44599  rp-fakeimass  44716  clublem  44813  grur1cld  45433  ee121  45690  ee122  45691  rspsbc2  45719  ax6e2ndeq  45744  vd12  45785  vd13  45786  ee221  45835  ee212  45837  ee112  45840  ee211  45843  ee210  45845  ee201  45847  ee120  45849  ee021  45851  ee012  45853  ee102  45855  ee03  45925  ee31  45936  ee31an  45938  ee123  45947  ax6e2ndeqVD  46093  ax6e2ndeqALT  46115  refsum2cnlem1  46270  fiiuncl  46298  eliin2f  46334  disjrnmpt2  46418  disjinfi  46422  rnmptbdlem  46482  allbutfi  46619  infxrunb3rnmpt  46653  infrpgernmpt  46690  monoordxrv  46706  mccl  46825  constlimc  46851  limclner  46876  xlimmnfvlem1  47057  xlimpnfvlem1  47061  ioodvbdlimc1lem2  47157  ioodvbdlimc2lem  47159  dvnprodlem3  47173  stoweidlem31  47256  pwsal  47540  prsal  47543  sge0pnffigt  47621  sge0ltfirp  47625  0ome  47754  hoicvrrex  47781  hoidmvle  47825  ovnhoilem1  47826  ovnlecvr2  47835  smflimlem3  47998  ormkglobd  48102  tmachlem-agreeprod  48162  funressnfv  48328  euoreqb  48395  ndmaovass  48491  afv2orxorb  48513  otiunsndisjX  48564  nltle2tri  48598  nnmul2b  48616  m1modmmod  48649  smonoord  48662  iccpartigtl  48720  icceuelpartlem  48732  iccpartnel  48735  sprsymrelfolem2  48790  prproropf1olem4  48803  paireqne  48808  reupr  48819  reuopreuprim  48823  nprmmul3  48826  fmtnoprmfac1  48865  fmtnoprmfac2  48867  prmdvdsfmtnof1lem2  48885  31prm  48897  lighneallem3  48907  lighneallem4b  48909  lighneallem4  48910  lighneal  48911  nprmdvdsfacm1lem2  48921  ppivalnnnprm  48928  nn0o1gt2ALTV  49007  nn0oALTV  49009  odd2prm2  49031  even3prm2  49032  fpprwppr  49052  stgoldbwt  49089  sbgoldbwt  49090  sbgoldbalt  49094  sbgoldbo  49100  nnsum3primesgbe  49105  wtgoldbnnsum4prm  49115  bgoldbnnsum3prm  49117  bgoldbtbndlem2  49119  bgoldbtbndlem3  49120  bgoldbtbndlem4  49121  bgoldbtbnd  49122  bgoldbachlt  49126  tgblthelfgott  49128  dfclnbgr6  49169  grimco  49202  uhgrimisgrgric  49244  grtriprop  49254  usgrgrtrirex  49263  isubgr3stgrlem6  49284  isubgr3stgrlem8  49286  grlimprclnbgr  49309  grlimgrtri  49316  gpgedg2ov  49379  gpg5nbgrvtx03starlem1  49381  gpg5nbgrvtx03starlem2  49382  gpg5nbgrvtx03starlem3  49383  gpg5nbgrvtx13starlem1  49384  gpg5nbgrvtx13starlem2  49385  gpg5nbgrvtx13starlem3  49386  gpgcubic  49392  gpg5nbgr3star  49394  gpgprismgr4cycllem7  49414  pgnbgreunbgrlem2  49430  gpg5edgnedg  49443  upgrwlkupwlk  49453  rngccatidALTV  49584  ringccatidALTV  49618  lincdifsn  49751  lindslinindimp2lem1  49785  lindsrng01  49795  ldepsnlinc  49835  blen1b  49915  nn0sumshdiglemB  49947  nn0sumshdiglem1  49948  reorelicc  50037  rrx2plord2  50050  rrxlinesc  50063  line2ylem  50078  line2xlem  50080  thincmon  50783  thincepi  50784