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  2458  ax12vALT  2504  nfsb4t  2534  moexexlem  2657  pm2.61da3ne  3050  ralrimivw  3164  rexlimdvw  3174  reximdv  3183  vtocl2d  3531  reuind  3719  reuan  3853  2reu4  4490  rabeqsnd  4640  tppreqb  4778  ssprsseq  4796  n0snor2el  4803  prnebg  4826  prel12g  4834  elpreqprlem  4836  3elpr2eq  4876  disjord  5103  disjiund  5105  dtruALT2  5346  exneq  5422  propssopi  5496  opthhausdorff  5505  fr0  5644  ssrel2  5776  poltletr  6137  reuop  6301  ordsssuc2  6461  ordnbtwn  6463  ndmfv  6920  fveqres  6932  fmptco  7132  funsndifnop  7155  tpres  7206  fntpb  7214  elunirn  7256  isof1oopb  7334  ndmovord  7613  ordsucelsuc  7827  tfinds  7865  tfindsg  7866  limomss  7876  findsg  7903  finds1  7905  xpexr  7924  resf1extb  7940  bropopvvv  8094  bropfvvvvlem  8095  bropfvvvv  8096  soxp  8134  poseq  8163  suppun  8189  extmptsuppeq  8193  funsssuppss  8195  suppss  8199  suppss2  8205  suppssfv  8207  suppco  8211  mpoxopynvov0  8223  smofvon2  8352  oaordi  8540  oawordeulem  8548  odi  8573  omeulem1  8576  brdomg  8964  snmapen  9045  fopwdom  9083  fodomr  9126  mapxpen  9141  infensuc  9153  fineqvlem  9236  fineqv  9237  fodomfir  9297  finsschain  9326  fsuppun  9357  fsuppunbi  9359  funsnfsupp  9362  dffi3  9401  fisup2g  9439  fisupcl  9440  fiinf2g  9472  infsupprpr  9476  wemapso2  9525  epnsym  9588  en3lplem2  9592  preleqg  9594  inf3lemd  9606  r1ordg  9760  r1val1  9768  r1pw  9827  r1pwALT  9828  rankxplim3  9863  eldju2ndl  9929  eldju2ndr  9930  carddomi2  9975  fidomtri  9998  alephon  10072  alephcard  10073  alephnbtwn  10074  alephordi  10077  iunfictbso  10117  fin23lem30  10344  fin1a2lem10  10411  axdc3lem2  10453  axdc3lem4  10455  alephval2  10575  cfpwsdom  10587  axextnd  10594  axrepnd  10597  axpownd  10604  axregnd  10607  axinfndlem1  10608  fpwwe2lem11  10644  wunfi  10724  addnidpi  10904  pinq  10930  mulgt0sr  11108  dedekind  11391  indval0  12240  nnind  12269  nn1m1nn  12272  nn0n0n1ge2b  12591  nn0lt2  12677  nn0le2is012  12678  uzm1  12914  uzinfi  12970  nn01to3  12983  xrltnsym  13180  xrlttri  13182  xrlttr  13183  qbtwnxr  13244  xltnegi  13260  xnn0xaddcl  13279  xlt2add  13304  xrsupsslem  13351  xrinfmsslem  13352  xrub  13356  reltxrnmnf  13387  fzdif1  13652  fzospliti  13739  elfzonlteqm1  13789  fzoopth  13810  elfznelfzo  13821  injresinjlem  13838  injresinj  13839  modfzo0difsn  13999  addmodlteq  14002  ssnn0fi  14041  fsuppmapnn0fiub0  14049  suppssfz  14050  seqfveq2  14080  monoord  14088  seqf1o  14099  seqhomo  14105  expnngt1  14297  faclbnd4lem4  14352  hasheqf1oi  14407  hashrabsn1  14430  hashgt0elex  14457  hash1snb  14476  hashf1lem2  14513  hashf1  14514  seqcoll  14521  hashle2pr  14534  pr2pwpr  14536  hashge2el2difr  14538  swrdnnn0nd  14718  swrdnd0  14719  pfxnd0  14750  swrdswrd  14766  pfxccatin12lem3  14793  pfxccat3  14795  swrdccat3blem  14800  repsdf2  14841  repswsymballbi  14843  cshw0  14857  cshwmodn  14858  cshwn  14860  cshwcl  14861  cshwlen  14862  cshw1  14885  2cshwcshw  14888  cshimadifsn  14892  s3sndisj  15030  s3iunsndisj  15031  relexprelg  15101  relexpnndm  15104  relexpaddg  15116  relexpaddd  15117  rtrclreclem4  15124  relexpindlem  15126  rexuz3  15426  rexanuz2  15427  limsupgre  15558  rlimconst  15621  caurcvg  15754  caucvg  15756  sumss  15801  fsumcl2lem  15808  modfsummods  15871  fsumrlim  15889  fsumo1  15890  fprodcl2lem  16030  dvdsaddre2b  16390  dvdsabseq  16396  mod2eq1n2dvds  16430  nno  16465  sumeven  16470  sumodd  16471  nn0rppwr  16644  nn0seqcvgd  16653  lcmdvds  16691  lcmfunsnlem2  16723  lcmfunsnlem  16724  divgcdcoprm0  16748  ge2nprmge4  16785  exprmfct  16788  rpexp1i  16807  prm23lt5  16899  prm23ge5  16900  pcz  16966  pcadd  16974  pcmptcl  16976  oddprmdvds  16988  prmgaplem6  17141  prmgaplem7  17142  cshwshashlem1  17180  cshwsdisj  17183  prmlem0  17190  setsstruct  17261  ressress  17332  initoeu2lem2  18097  mgm2nsgrplem2  19012  mgm2nsgrplem3  19013  dfgrp2e  19061  dfgrp3e  19137  cyccom  19305  symgextf1  19522  gsmsymgrfix  19529  gsmsymgreq  19533  sylow1lem1  19699  efgsf  19830  efgrelexlema  19850  dprdss  20132  ablfac1eulem  20175  01eq0ringOLD  20666  nrhmzr  20673  funcrngcsetcALT  20777  lssssr  21112  isfieldidl  21423  psgnodpm  21775  psrvscafval  22135  mplcoe1  22225  mplcoe5  22228  mpfrcl  22273  mamudm  22589  matmulcell  22639  dmatmul  22691  scmatsgrp1  22716  mavmuldm  22744  mavmulsolcl  22745  mdetunilem9  22814  cramerlem3  22883  cramer0  22884  chpscmatgsumbin  23038  chp0mat  23040  fvmptnn04ifc  23046  fvmptnn04ifd  23047  epttop  23203  neiptopnei  23326  fiuncmp  23598  1stcrest  23647  kgenss  23737  hmeofval  23952  fbun  24034  fgss2  24068  filuni  24079  filssufilg  24105  filufint  24114  hausflimi  24174  hausflim  24175  hauspwpwf1  24181  fclscmp  24224  alexsubALTlem4  24244  ptcmplem3  24248  ptcmplem5  24250  cstucnd  24477  isxmet2d  24521  imasdsf1olem  24567  blfps  24600  blf  24601  metrest  24718  nrginvrcn  24886  nmoge0  24915  nmoleub  24925  fsumcn  25066  cmetcaulem  25484  iscmet3  25489  iscmet2  25490  bcthlem2  25521  ovolicc2lem3  25715  itg2seq  25938  itg2splitlem  25944  itgeq1fOLD  25968  itgeq2  25974  iblcnlem  25985  itgfsum  26023  limcnlp  26074  perfdvf  26099  dvnres  26127  dvmptfsum  26171  c1lip1  26193  dvply2g  26483  taylply2  26568  abelth  26641  cxpsqrtth  26932  rlimcnp  27167  xrlimcnp  27170  jensen  27190  ppiublem1  27403  dchrelbas3  27439  bcmono  27478  zabsle1  27497  gausslemma2dlem0f  27562  gausslemma2dlem1a  27566  gausslemma2dlem4  27570  lgsquad2lem2  27586  2lgslem1a1  27590  2lgslem3  27605  2lgs  27608  2lgsoddprm  27617  2sqlem10  27629  2sqnn  27640  addsqnreup  27644  2sqreultblem  27649  2sqreunnltblem  27652  pntrsumbnd2  27768  pntpbnd1  27787  pntlem3  27810  nolesgn2o  27872  noetalem1  27942  bday0b  28043  leftf  28085  rightf  28086  oldss  28100  addcutslem  28207  negcut  28269  mulcutlem  28361  n0s0suc  28572  n0fincut  28585  n0s0m1  28592  nn1m1nns  28604  axcontlem7  29357  elntg2  29372  ausgrusgrb  29552  usgredg2v  29614  lfuhgr1v0e  29641  subumgredg2  29672  upgrreslem  29691  umgrreslem  29692  fusgrfisbase  29715  nbuhgr  29730  uhgrnbgr0nb  29741  nbgr0edglem  29743  nbgr1vtx  29745  cusgredg  29811  cusgrsizeinds  29839  sizusglecusg  29850  finsumvtxdg2size  29937  ewlkle  29992  upgriswlk  30027  pthdivtx  30113  dfpth2  30115  usgr2trlncl  30146  crctcshwlkn0lem4  30199  wwlksn  30223  iswwlksnon  30239  iswspthsnon  30242  wwlksm1edg  30267  wwlksnfi  30292  2pthdlem1  30316  umgr2wlk  30335  umgrclwwlkge2  30379  clwlkclwwlklem2a  30386  clwlkclwwlk  30390  clwlkclwwlkf1lem2  30393  clwlkclwwlkf  30396  clwwisshclwws  30403  clwwlknlbonbgr1  30427  clwwlknon0  30481  clwwlknonel  30483  clwwlknonex2e  30498  3pthdlem1  30552  eupth2  30627  nfrgr2v  30660  frgr3vlem1  30661  1to2vfriswmgr  30667  1to3vfriswmgr  30668  vdgn1frgrv2  30684  frgrncvvdeqlem9  30695  frgrwopreglem4a  30698  frgrregorufr0  30712  frgrregorufr  30713  2wspmdisj  30725  2clwwlk2clwwlklem  30734  frgrreggt1  30781  frgrreg  30782  frgrregord13  30784  aevdemo  30848  shsvs  31712  0cnop  32368  0cnfn  32369  cnlnssadj  32469  ssmd1  32700  ssmd2  32701  atexch  32770  mdsymlem4  32795  sumdmdlem  32807  ifeqeqx  32925  fmptcof2  33039  padct  33100  nnindf  33201  drng0mxidl  33789  constr01  34163  pwsiga  34551  pwldsys  34579  ldsysgenld  34582  fiunelros  34596  breprexp  35052  bnj151  35297  bnj594  35332  bnj600  35339  trssfir1om  35532  rankscottu  35547  trssfir1omregs  35573  subfacp1lem6  35698  erdszelem8  35711  cvmliftlem7  35804  cvmliftlem10  35807  cvmlift2lem12  35827  sat1el2xp  35892  mrsubfval  36021  msubfval  36037  mclsssvlem  36075  antnestlaw2  36205  funpartfv  36458  endofsegid  36598  broutsideof2  36635  a1i24  36854  nn0prpwlem  36874  nn0prpw  36875  ordcmp  36999  findreccl  37005  axtcond  37030  dfttc2g  37058  dfttc4lem2  37081  bj-cbvaw  37304  bj-cbveaw  37306  bj-ax6e  37331  bj-ax12v3ALT  37352  bj-xpnzex  37636  bj-ideqg1  37849  rdgssun  38065  finxp00  38089  domalom  38091  isinf2  38092  fvineqsneq  38099  wl-spae  38217  wl-nfs1t  38233  poimirlem27  38339  ovoliunnfl  38354  voliunnfl  38356  volsupnfl  38357  itg2addnclem3  38365  itg2addnc  38366  ftc1anc  38393  areacirclem1  38400  sdclem2  38434  fdc  38437  mettrifi  38449  isexid2  38547  zerdivemp1x  38639  smprngopr  38744  mpobi123f  38852  mptbi12f  38856  ac6s6  38862  relcnveq3  39017  mopickr  39061  elrelscnveq3  39317  disjlem14  39591  jca3  39671  ax12fromc15  39720  hbequid  39724  dvelimf-o  39744  ax12eq  39756  ax12el  39757  ax12indalem  39760  ax12inda2ALT  39761  ax12inda2  39762  lfl1dim  39936  lfl1dim2N  39937  lkreqN  39985  cvrexchlem  40234  ps-2  40293  paddasslem14  40648  idldil  40929  isltrn2N  40935  cdleme25a  41168  dibglbN  41981  dihlsscpre  42049  dvh4dimlem  42258  lcfl7N  42316  mapdval2N  42445  dvrelog2b  42874  aks6d1c6lem3  42980  monotoddzzfi  43710  onov0suclim  44042  onmcl  44099  omabs2  44100  tfsconcat0b  44114  naddgeoa  44162  rp-fakeimass  44279  clublem  44377  grur1cld  44997  ee121  45255  ee122  45256  rspsbc2  45284  ax6e2ndeq  45309  vd12  45350  vd13  45351  ee221  45400  ee212  45402  ee112  45405  ee211  45408  ee210  45410  ee201  45412  ee120  45414  ee021  45416  ee012  45418  ee102  45420  ee03  45490  ee31  45501  ee31an  45503  ee123  45512  ax6e2ndeqVD  45658  ax6e2ndeqALT  45680  refsum2cnlem1  45798  fiiuncl  45826  eliin2f  45863  disjrnmpt2  45947  disjinfi  45951  rnmptbdlem  46011  allbutfi  46149  infxrunb3rnmpt  46183  infrpgernmpt  46220  monoordxrv  46236  mccl  46355  constlimc  46381  limclner  46406  xlimmnfvlem1  46587  xlimpnfvlem1  46591  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  dvnprodlem3  46703  stoweidlem31  46786  pwsal  47070  prsal  47073  sge0pnffigt  47151  sge0ltfirp  47155  0ome  47284  hoicvrrex  47311  hoidmvle  47355  ovnhoilem1  47356  ovnlecvr2  47365  smflimlem3  47528  ormkglobd  47632  chnsubseqword  47635  funressnfv  47821  euoreqb  47887  ndmaovass  47984  afv2orxorb  48006  otiunsndisjX  48057  nltle2tri  48091  nnmul2b  48109  m1modmmod  48142  smonoord  48155  iccpartigtl  48213  icceuelpartlem  48225  iccpartnel  48228  sprsymrelfolem2  48283  prproropf1olem4  48296  paireqne  48301  reupr  48312  reuopreuprim  48316  nprmmul3  48319  fmtnoprmfac1  48358  fmtnoprmfac2  48360  prmdvdsfmtnof1lem2  48378  31prm  48390  lighneallem3  48400  lighneallem4b  48402  lighneallem4  48403  lighneal  48404  nprmdvdsfacm1lem2  48414  ppivalnnnprm  48421  nn0o1gt2ALTV  48500  nn0oALTV  48502  odd2prm2  48524  even3prm2  48525  fpprwppr  48545  stgoldbwt  48582  sbgoldbwt  48583  sbgoldbalt  48587  sbgoldbo  48593  nnsum3primesgbe  48598  wtgoldbnnsum4prm  48608  bgoldbnnsum3prm  48610  bgoldbtbndlem2  48612  bgoldbtbndlem3  48613  bgoldbtbndlem4  48614  bgoldbtbnd  48615  bgoldbachlt  48619  tgblthelfgott  48621  dfclnbgr6  48662  grimco  48695  uhgrimisgrgric  48737  grtriprop  48747  usgrgrtrirex  48756  isubgr3stgrlem6  48777  isubgr3stgrlem8  48779  grlimprclnbgr  48802  grlimgrtri  48809  gpgedg2ov  48872  gpg5nbgrvtx03starlem1  48874  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx03starlem3  48876  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem2  48878  gpg5nbgrvtx13starlem3  48879  gpgcubic  48885  gpg5nbgr3star  48887  gpgprismgr4cycllem7  48907  pgnbgreunbgrlem2  48923  gpg5edgnedg  48936  upgrwlkupwlk  48946  rngccatidALTV  49078  ringccatidALTV  49112  lincdifsn  49245  lindslinindimp2lem1  49279  lindsrng01  49289  ldepsnlinc  49329  blen1b  49409  nn0sumshdiglemB  49441  nn0sumshdiglem1  49442  reorelicc  49531  rrx2xpref1o  49539  rrx2plord2  49543  rrxlinesc  49556  line2ylem  49572  line2xlem  49574  thincmon  50252  thincepi  50253