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  2454  ax12vALT  2500  nfsb4t  2530  moexexlem  2653  pm2.61da3ne  3046  ralrimivw  3160  rexlimdvw  3170  reximdv  3179  vtocl2d  3526  reuind  3714  reuan  3847  2reu4  4483  rabeqsnd  4633  tppreqb  4771  ssprsseq  4789  n0snor2el  4796  prnebg  4819  prel12g  4827  elpreqprlem  4829  3elpr2eq  4869  disjord  5096  disjiund  5098  dtruALT2  5339  exneq  5415  propssopi  5489  opthhausdorff  5498  fr0  5637  ssrel2  5769  poltletr  6130  reuop  6295  ordsssuc2  6455  ordnbtwn  6457  ndmfv  6914  fveqres  6926  fmptco  7127  funsndifnop  7152  tpres  7204  fntpb  7212  elunirn  7252  isof1oopb  7330  ndmovord  7608  ordsucelsuc  7822  tfinds  7860  tfindsg  7861  limomss  7871  findsg  7898  finds1  7900  xpexr  7919  resf1extb  7935  bropopvvv  8091  bropfvvvvlem  8092  bropfvvvv  8093  soxp  8131  poseq  8160  suppun  8186  extmptsuppeq  8190  funsssuppss  8192  suppss  8196  suppss2  8202  suppssfv  8204  suppco  8208  mpoxopynvov0  8220  smofvon2  8349  oaordi  8537  oawordeulem  8545  odi  8570  omeulem1  8573  brdomg  8968  snmapen  9049  fopwdom  9087  fodomr  9130  mapxpen  9145  infensuc  9157  fineqvlem  9240  fineqv  9241  fodomfir  9301  finsschain  9330  fsuppun  9361  fsuppunbi  9363  funsnfsupp  9366  dffi3  9405  fisup2g  9443  fisupcl  9444  fiinf2g  9476  infsupprpr  9480  wemapso2  9529  epnsym  9592  en3lplem2  9596  preleqg  9598  inf3lemd  9610  r1ordg  9764  r1val1  9772  r1pw  9831  r1pwALT  9832  rankxplim3  9867  eldju2ndl  9933  eldju2ndr  9934  carddomi2  9979  fidomtri  10002  alephon  10076  alephcard  10077  alephnbtwn  10078  alephordi  10081  iunfictbso  10121  fin23lem30  10348  fin1a2lem10  10415  axdc3lem2  10457  axdc3lem4  10459  alephval2  10585  cfpwsdom  10597  axextnd  10604  axrepnd  10607  axpownd  10614  axregnd  10617  axinfndlem1  10618  fpwwe2lem11  10654  wunfi  10734  addnidpi  10914  pinq  10940  mulgt0sr  11118  dedekind  11401  indval0  12250  nnind  12279  nn1m1nn  12282  nn0n0n1ge2b  12601  nn0lt2  12688  nn0le2is012  12689  uzm1  12925  uzinfi  12981  nn01to3  12994  xrltnsym  13192  xrlttri  13194  xrlttr  13195  qbtwnxr  13256  xltnegi  13272  xnn0xaddcl  13291  xlt2add  13316  xrsupsslem  13363  xrinfmsslem  13364  xrub  13368  reltxrnmnf  13399  fzdif1  13664  fzospliti  13751  elfzonlteqm1  13801  fzoopth  13822  elfznelfzo  13833  injresinjlem  13850  injresinj  13851  modfzo0difsn  14011  addmodlteq  14014  ssnn0fi  14053  fsuppmapnn0fiub0  14061  suppssfz  14062  seqfveq2  14092  monoord  14100  seqf1o  14111  seqhomo  14117  expnngt1  14309  faclbnd4lem4  14364  hasheqf1oi  14419  hashrabsn1  14442  hashgt0elex  14469  hash1snb  14488  hashf1lem2  14525  hashf1  14526  seqcoll  14533  hashle2pr  14546  pr2pwpr  14548  hashge2el2difr  14550  swrdnnn0nd  14730  swrdnd0  14731  pfxnd0  14762  swrdswrd  14778  pfxccatin12lem3  14805  pfxccat3  14807  swrdccat3blem  14812  repsdf2  14853  repswsymballbi  14855  cshw0  14869  cshwmodn  14870  cshwn  14872  cshwcl  14873  cshwlen  14874  cshw1  14897  2cshwcshw  14900  cshimadifsn  14904  s3sndisj  15044  s3iunsndisj  15045  relexprelg  15115  relexpnndm  15118  relexpaddg  15130  relexpaddd  15131  rtrclreclem4  15138  relexpindlem  15140  rexuz3  15440  rexanuz2  15441  limsupgre  15572  rlimconst  15635  caurcvg  15768  caucvg  15770  sumss  15814  fsumcl2lem  15821  modfsummods  15884  fsumrlim  15902  fsumo1  15903  fprodcl2lem  16043  dvdsaddre2b  16403  dvdsabseq  16409  mod2eq1n2dvds  16443  nno  16478  sumeven  16483  sumodd  16484  nn0rppwr  16657  nn0seqcvgd  16666  lcmdvds  16704  lcmfunsnlem2  16736  lcmfunsnlem  16737  divgcdcoprm0  16761  ge2nprmge4  16798  exprmfct  16801  rpexp1i  16820  prm23lt5  16912  prm23ge5  16913  pcz  16979  pcadd  16987  pcmptcl  16989  oddprmdvds  17001  prmgaplem6  17154  prmgaplem7  17155  cshwshashlem1  17193  cshwsdisj  17196  prmlem0  17203  setsstruct  17274  ressress  17345  initoeu2lem2  18110  mgmn0plusgf  18747  mgm2nsgrplem2  19037  mgm2nsgrplem3  19038  dfgrp2e  19093  dfgrp3e  19169  cyccom  19337  symgextf1  19554  gsmsymgrfix  19561  gsmsymgreq  19565  sylow1lem1  19731  efgsf  19862  efgrelexlema  19882  dprdss  20164  ablfac1eulem  20207  01eq0ringOLD  20698  nrhmzr  20705  funcrngcsetcALT  20809  lssssr  21144  isfieldidl  21455  psgnodpm  21807  psrvscafval  22169  mplcoe1  22259  mplcoe5  22262  mpfrcl  22307  mamudm  22623  matmulcell  22673  dmatmul  22725  scmatsgrp1  22750  mavmuldm  22778  mavmulsolcl  22779  mdetunilem9  22848  cramerlem3  22920  cramer0  22921  chpscmatgsumbin  23075  chp0mat  23077  fvmptnn04ifc  23083  fvmptnn04ifd  23084  epttop  23240  neiptopnei  23363  fiuncmp  23635  1stcrest  23684  kgenss  23775  hmeofval  23990  fbun  24072  fgss2  24106  filuni  24117  filssufilg  24143  filufint  24152  hausflimi  24212  hausflim  24213  hauspwpwf1  24219  fclscmp  24262  alexsubALTlem4  24282  ptcmplem3  24286  ptcmplem5  24288  cstucnd  24515  isxmet2d  24559  imasdsf1olem  24605  blfps  24638  blf  24639  metrest  24756  nrginvrcn  24924  nmoge0  24953  nmoleub  24963  fsumcn  25104  cmetcaulem  25522  iscmet3  25527  iscmet2  25528  bcthlem2  25559  ovolicc2lem3  25753  itg2seq  25976  itg2splitlem  25982  itgeq1fOLD  26006  itgeq2  26012  iblcnlem  26023  itgfsum  26061  limcnlp  26112  perfdvf  26137  dvnres  26165  dvmptfsum  26209  c1lip1  26231  dvply2g  26522  taylply2  26611  abelth  26684  cxpsqrtth  26975  rlimcnp  27210  xrlimcnp  27213  jensen  27233  ppiublem1  27446  dchrelbas3  27482  bcmono  27521  zabsle1  27540  gausslemma2dlem0f  27605  gausslemma2dlem1a  27609  gausslemma2dlem4  27613  lgsquad2lem2  27629  2lgslem1a1  27633  2lgslem3  27648  2lgs  27651  2lgsoddprm  27660  2sqlem10  27672  2sqnn  27683  addsqnreup  27687  2sqreultblem  27692  2sqreunnltblem  27695  pntrsumbnd2  27811  pntpbnd1  27830  pntlem3  27853  nolesgn2o  27915  noetalem1  27985  bday0b  28086  leftf  28128  rightf  28129  oldss  28143  addcutslem  28250  negcut  28312  mulcutlem  28404  n0s0suc  28615  n0fincut  28628  n0s0m1  28635  nn1m1nns  28647  axcontlem7  29435  elntg2  29450  ausgrusgrb  29633  usgredg2v  29695  lfuhgr1v0e  29722  subumgredg2  29753  upgrreslem  29772  umgrreslem  29773  fusgrfisbase  29796  nbuhgr  29811  uhgrnbgr0nb  29822  nbgr0edglem  29824  nbgr1vtx  29826  cusgredg  29892  cusgrsizeinds  29920  sizusglecusg  29931  finsumvtxdg2size  30018  ewlkle  30073  upgriswlk  30108  pthdivtx  30199  dfpth2  30201  usgr2trlncl  30233  crctcshwlkn0lem4  30289  wwlksn  30313  iswwlksnon  30329  iswspthsnon  30332  wwlksm1edg  30357  wwlksnfi  30382  2pthdlem1  30406  umgr2wlk  30425  umgrclwwlkge2  30469  clwlkclwwlklem2a  30476  clwlkclwwlk  30480  clwlkclwwlkf1lem2  30483  clwlkclwwlkf  30486  clwwisshclwws  30493  clwwlknlbonbgr1  30517  clwwlknon0  30571  clwwlknonel  30573  clwwlknonex2e  30588  3pthdlem1  30652  eupth2  30727  nfrgr2v  30760  frgr3vlem1  30761  1to2vfriswmgr  30767  1to3vfriswmgr  30768  vdgn1frgrv2  30784  frgrncvvdeqlem9  30795  frgrwopreglem4a  30798  frgrregorufr0  30812  frgrregorufr  30813  2wspmdisj  30825  2clwwlk2clwwlklem  30834  frgrreggt1  30881  frgrreg  30882  frgrregord13  30884  aevdemo  30948  shsvs  31812  0cnop  32468  0cnfn  32469  cnlnssadj  32569  ssmd1  32800  ssmd2  32801  atexch  32870  mdsymlem4  32895  sumdmdlem  32907  ifeqeqx  33025  fmptcof2  33138  padct  33197  nnindf  33298  drng0mxidl  33886  constr01  34260  pwsiga  34648  pwldsys  34676  ldsysgenld  34679  fiunelros  34693  breprexp  35149  bnj151  35394  bnj594  35429  bnj600  35436  trssfir1om  35629  rankscottu  35644  trssfir1omregs  35670  subfacp1lem6  35772  erdszelem8  35785  cvmliftlem7  35878  cvmliftlem10  35881  cvmlift2lem12  35901  sat1el2xp  35966  mrsubfval  36095  msubfval  36111  mclsssvlem  36149  antnestlaw2  36279  funpartfv  36532  endofsegid  36673  broutsideof2  36710  a1i24  36929  nn0prpwlem  36949  nn0prpw  36950  ordcmp  37074  findreccl  37080  axtcond  37105  dfttc2g  37133  dfttc4lem2  37156  bj-cbvaw  37379  bj-cbveaw  37381  bj-ax6e  37406  bj-ax12v3ALT  37427  bj-xpnzex  37711  bj-ideqg1  37924  rdgssun  38140  finxp00  38164  domalom  38166  isinf2  38167  fvineqsneq  38174  wl-spae  38292  wl-nfs1t  38308  poimirlem27  38404  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  itg2addnclem3  38430  itg2addnc  38431  ftc1anc  38458  areacirclem1  38465  sdclem2  38500  fdc  38503  mettrifi  38515  isexid2  38613  zerdivemp1x  38705  smprngopr  38810  mpobi123f  38918  mptbi12f  38922  ac6s6  38928  relcnveq3  39083  mopickr  39127  elrelscnveq3  39383  disjlem14  39657  jca3  39737  ax12fromc15  39786  hbequid  39790  dvelimf-o  39810  ax12eq  39822  ax12el  39823  ax12indalem  39826  ax12inda2ALT  39827  ax12inda2  39828  lfl1dim  40002  lfl1dim2N  40003  lkreqN  40051  cvrexchlem  40300  ps-2  40359  paddasslem14  40714  idldil  40995  isltrn2N  41001  cdleme25a  41234  dibglbN  42047  dihlsscpre  42115  dvh4dimlem  42324  lcfl7N  42382  mapdval2N  42511  dvrelog2b  42940  aks6d1c6lem3  43046  monotoddzzfi  43791  onov0suclim  44123  onmcl  44180  omabs2  44181  tfsconcat0b  44195  naddgeoa  44243  rp-fakeimass  44360  clublem  44458  grur1cld  45078  ee121  45336  ee122  45337  rspsbc2  45365  ax6e2ndeq  45390  vd12  45431  vd13  45432  ee221  45481  ee212  45483  ee112  45486  ee211  45489  ee210  45491  ee201  45493  ee120  45495  ee021  45497  ee012  45499  ee102  45501  ee03  45571  ee31  45582  ee31an  45584  ee123  45593  ax6e2ndeqVD  45739  ax6e2ndeqALT  45761  refsum2cnlem1  45879  fiiuncl  45907  eliin2f  45944  disjrnmpt2  46028  disjinfi  46032  rnmptbdlem  46092  allbutfi  46230  infxrunb3rnmpt  46264  infrpgernmpt  46301  monoordxrv  46317  mccl  46436  constlimc  46462  limclner  46487  xlimmnfvlem1  46668  xlimpnfvlem1  46672  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvnprodlem3  46784  stoweidlem31  46867  pwsal  47151  prsal  47154  sge0pnffigt  47232  sge0ltfirp  47236  0ome  47365  hoicvrrex  47392  hoidmvle  47436  ovnhoilem1  47437  ovnlecvr2  47446  smflimlem3  47609  ormkglobd  47713  tmachlem-agreeprod  47773  funressnfv  47939  euoreqb  48005  ndmaovass  48102  afv2orxorb  48124  otiunsndisjX  48175  nltle2tri  48209  nnmul2b  48227  m1modmmod  48260  smonoord  48273  iccpartigtl  48331  icceuelpartlem  48343  iccpartnel  48346  sprsymrelfolem2  48401  prproropf1olem4  48414  paireqne  48419  reupr  48430  reuopreuprim  48434  nprmmul3  48437  fmtnoprmfac1  48476  fmtnoprmfac2  48478  prmdvdsfmtnof1lem2  48496  31prm  48508  lighneallem3  48518  lighneallem4b  48520  lighneallem4  48521  lighneal  48522  nprmdvdsfacm1lem2  48532  ppivalnnnprm  48539  nn0o1gt2ALTV  48618  nn0oALTV  48620  odd2prm2  48642  even3prm2  48643  fpprwppr  48663  stgoldbwt  48700  sbgoldbwt  48701  sbgoldbalt  48705  sbgoldbo  48711  nnsum3primesgbe  48716  wtgoldbnnsum4prm  48726  bgoldbnnsum3prm  48728  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  bgoldbtbndlem4  48732  bgoldbtbnd  48733  bgoldbachlt  48737  tgblthelfgott  48739  dfclnbgr6  48780  grimco  48813  uhgrimisgrgric  48855  grtriprop  48865  usgrgrtrirex  48874  isubgr3stgrlem6  48895  isubgr3stgrlem8  48897  grlimprclnbgr  48920  grlimgrtri  48927  gpgedg2ov  48990  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem2  48996  gpg5nbgrvtx13starlem3  48997  gpgcubic  49003  gpg5nbgr3star  49005  gpgprismgr4cycllem7  49025  pgnbgreunbgrlem2  49041  gpg5edgnedg  49054  upgrwlkupwlk  49064  rngccatidALTV  49195  ringccatidALTV  49229  lincdifsn  49362  lindslinindimp2lem1  49396  lindsrng01  49406  ldepsnlinc  49446  blen1b  49526  nn0sumshdiglemB  49558  nn0sumshdiglem1  49559  reorelicc  49648  rrx2xpref1o  49656  rrx2plord2  49660  rrxlinesc  49673  line2ylem  49689  line2xlem  49691  thincmon  50367  thincepi  50368