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  186  mtod  199  imbi2d  341  adantr  481  jctild  530  jctird  531  anbi2d  636  anbi1d  637  pm3.4  815  impsingle  1634  meredith  1648  stdpc4  2079  ax12  2431  ax12vALT  2477  nfsb4t  2507  moexexlem  2630  pm2.61da3ne  3024  ralrimivw  3136  rexlimdvw  3146  reximdv  3155  vtocl2d  3510  reuind  3701  reuan  3835  2reu4  4459  rabeqsnd  4608  tppreqb  4745  ssprsseq  4763  n0snor2el  4771  prnebg  4794  prel12g  4802  elpreqprlem  4804  3elpr2eq  4844  disjord  5068  disjiund  5070  dtruALT2  5306  exneq  5382  propssopi  5456  opthhausdorff  5465  fr0  5603  ssrel2  5735  poltletr  6089  reuop  6251  ordsssuc2  6410  ordnbtwn  6412  ndmfv  6866  fveqres  6878  fmptco  7078  funsndifnop  7101  tpres  7152  fntpb  7160  elunirn  7202  isof1oopb  7276  ndmovord  7553  ordsucelsuc  7769  tfinds  7807  tfindsg  7808  limomss  7818  findsg  7844  finds1  7846  xpexr  7865  resf1extb  7881  bropopvvv  8036  bropfvvvvlem  8037  bropfvvvv  8038  soxp  8076  poseq  8105  suppun  8131  extmptsuppeq  8135  funsssuppss  8137  suppss  8141  suppss2  8147  suppssfv  8149  suppco  8153  mpoxopynvov0  8165  smofvon2  8293  oaordi  8478  oawordeulem  8486  odi  8511  omeulem1  8514  brdomg  8902  snmapen  8982  fopwdom  9020  fodomr  9063  mapxpen  9078  infensuc  9090  fineqvlem  9173  fineqv  9174  fodomfir  9235  finsschain  9266  fsuppun  9297  fsuppunbi  9299  funsnfsupp  9302  dffi3  9341  fisup2g  9379  fisupcl  9380  fiinf2g  9412  infsupprpr  9416  wemapso2  9465  epnsym  9528  en3lplem2  9532  preleqg  9534  inf3lemd  9546  r1ordg  9700  r1val1  9708  r1pw  9767  r1pwALT  9768  rankxplim3  9803  eldju2ndl  9846  eldju2ndr  9847  carddomi2  9892  fidomtri  9915  alephon  9989  alephcard  9990  alephnbtwn  9991  alephordi  9994  iunfictbso  10034  fin23lem30  10262  fin1a2lem10  10329  axdc3lem2  10371  axdc3lem4  10373  alephval2  10493  cfpwsdom  10505  axextnd  10512  axrepnd  10515  axpownd  10522  axregnd  10525  axinfndlem1  10526  fpwwe2lem11  10562  wunfi  10642  addnidpi  10822  pinq  10848  mulgt0sr  11026  dedekind  11307  indval0  12161  nnind  12190  nn1m1nn  12193  nn0n0n1ge2b  12504  nn0lt2  12590  nn0le2is012  12591  uzm1  12820  uzinfi  12876  nn01to3  12889  xrltnsym  13086  xrlttri  13088  xrlttr  13089  qbtwnxr  13150  xltnegi  13166  xnn0xaddcl  13185  xlt2add  13210  xrsupsslem  13257  xrinfmsslem  13258  xrub  13262  reltxrnmnf  13293  fzdif1  13557  fzospliti  13644  elfzonlteqm1  13694  fzoopth  13715  elfznelfzo  13726  injresinjlem  13743  injresinj  13744  modfzo0difsn  13903  addmodlteq  13906  ssnn0fi  13945  fsuppmapnn0fiub0  13953  suppssfz  13954  seqfveq2  13984  monoord  13992  seqf1o  14003  seqhomo  14009  expnngt1  14201  faclbnd4lem4  14256  hasheqf1oi  14311  hashrabsn1  14334  hashgt0elex  14361  hash1snb  14379  hashf1lem2  14416  hashf1  14417  seqcoll  14424  hashle2pr  14437  pr2pwpr  14439  hashge2el2difr  14441  swrdnnn0nd  14617  swrdnd0  14618  pfxnd0  14649  swrdswrd  14665  pfxccatin12lem3  14692  pfxccat3  14694  swrdccat3blem  14699  repsdf2  14738  repswsymballbi  14740  cshw0  14754  cshwmodn  14755  cshwn  14757  cshwcl  14758  cshwlen  14759  cshw1  14782  2cshwcshw  14785  cshimadifsn  14789  s3sndisj  14927  s3iunsndisj  14928  relexprelg  14998  relexpnndm  15001  relexpaddg  15013  relexpaddd  15014  rtrclreclem4  15021  relexpindlem  15023  rexuz3  15309  rexanuz2  15310  limsupgre  15441  rlimconst  15504  caurcvg  15637  caucvg  15639  sumss  15684  fsumcl2lem  15691  modfsummods  15754  fsumrlim  15772  fsumo1  15773  fprodcl2lem  15913  dvdsaddre2b  16274  dvdsabseq  16280  mod2eq1n2dvds  16314  nno  16349  sumeven  16354  sumodd  16355  nn0rppwr  16528  nn0seqcvgd  16537  lcmdvds  16575  lcmfunsnlem2  16607  lcmfunsnlem  16608  divgcdcoprm0  16632  ge2nprmge4  16669  exprmfct  16672  rpexp1i  16691  prm23lt5  16783  prm23ge5  16784  pcz  16850  pcadd  16858  pcmptcl  16860  oddprmdvds  16872  prmgaplem6  17025  prmgaplem7  17026  cshwshashlem1  17064  cshwsdisj  17067  prmlem0  17074  setsstruct  17144  ressress  17215  initoeu2lem2  17980  mgm2nsgrplem2  18888  mgm2nsgrplem3  18889  dfgrp2e  18937  dfgrp3e  19014  cyccom  19176  symgextf1  19394  gsmsymgrfix  19401  gsmsymgreq  19405  sylow1lem1  19571  efgsf  19702  efgrelexlema  19722  dprdss  20004  ablfac1eulem  20047  01eq0ringOLD  20510  nrhmzr  20516  funcrngcsetcALT  20620  lssssr  20951  psgnodpm  21570  psrvscafval  21930  mplcoe1  22020  mplcoe5  22023  mpfrcl  22068  mamudm  22385  matmulcell  22435  dmatmul  22487  scmatsgrp1  22512  mavmuldm  22540  mavmulsolcl  22541  mdetunilem9  22610  cramerlem3  22679  cramer0  22680  chpscmatgsumbin  22834  chp0mat  22836  fvmptnn04ifc  22842  fvmptnn04ifd  22843  epttop  22999  neiptopnei  23122  fiuncmp  23394  1stcrest  23443  kgenss  23533  hmeofval  23748  fbun  23830  fgss2  23864  filuni  23875  filssufilg  23901  filufint  23910  hausflimi  23970  hausflim  23971  hauspwpwf1  23977  fclscmp  24020  alexsubALTlem4  24040  ptcmplem3  24044  ptcmplem5  24046  cstucnd  24273  isxmet2d  24317  imasdsf1olem  24363  blfps  24396  blf  24397  metrest  24514  nrginvrcn  24682  nmoge0  24711  nmoleub  24721  fsumcn  24862  cmetcaulem  25280  iscmet3  25285  iscmet2  25286  bcthlem2  25317  ovolicc2lem3  25511  itg2seq  25734  itg2splitlem  25740  itgeq1fOLD  25764  itgeq2  25770  iblcnlem  25781  itgfsum  25819  limcnlp  25870  perfdvf  25895  dvnres  25923  dvmptfsum  25967  c1lip1  25989  dvply2g  26276  taylply2  26358  abelth  26431  cxpsqrtth  26719  rlimcnp  26954  xrlimcnp  26957  jensen  26977  ppiublem1  27190  dchrelbas3  27226  bcmono  27265  zabsle1  27284  gausslemma2dlem0f  27349  gausslemma2dlem1a  27353  gausslemma2dlem4  27357  lgsquad2lem2  27373  2lgslem1a1  27377  2lgslem3  27392  2lgs  27395  2lgsoddprm  27404  2sqlem10  27416  2sqnn  27427  addsqnreup  27431  2sqreultblem  27436  2sqreunnltblem  27439  pntrsumbnd2  27555  pntpbnd1  27574  pntlem3  27597  nolesgn2o  27660  noetalem1  27730  bday0b  27830  leftf  27872  rightf  27873  oldss  27887  addcutslem  27994  negcut  28056  mulcutlem  28148  n0s0suc  28359  n0fincut  28372  n0s0m1  28379  nn1m1nns  28391  axcontlem7  29064  elntg2  29079  ausgrusgrb  29259  usgredg2v  29321  lfuhgr1v0e  29348  subumgredg2  29379  upgrreslem  29398  umgrreslem  29399  fusgrfisbase  29422  nbuhgr  29437  uhgrnbgr0nb  29448  nbgr0edglem  29450  nbgr1vtx  29452  cusgredg  29518  cusgrsizeinds  29546  sizusglecusg  29557  finsumvtxdg2size  29644  ewlkle  29699  upgriswlk  29734  pthdivtx  29820  dfpth2  29822  usgr2trlncl  29853  crctcshwlkn0lem4  29906  wwlksn  29930  iswwlksnon  29946  iswspthsnon  29949  wwlksm1edg  29974  wwlksnfi  29999  2pthdlem1  30023  umgr2wlk  30042  umgrclwwlkge2  30086  clwlkclwwlklem2a  30093  clwlkclwwlk  30097  clwlkclwwlkf1lem2  30100  clwlkclwwlkf  30103  clwwisshclwws  30110  clwwlknlbonbgr1  30134  clwwlknon0  30188  clwwlknonel  30190  clwwlknonex2e  30205  3pthdlem1  30259  eupth2  30334  nfrgr2v  30367  frgr3vlem1  30368  1to2vfriswmgr  30374  1to3vfriswmgr  30375  vdgn1frgrv2  30391  frgrncvvdeqlem9  30402  frgrwopreglem4a  30405  frgrregorufr0  30419  frgrregorufr  30420  2wspmdisj  30432  2clwwlk2clwwlklem  30441  frgrreggt1  30488  frgrreg  30489  frgrregord13  30491  aevdemo  30555  shsvs  31419  0cnop  32075  0cnfn  32076  cnlnssadj  32176  ssmd1  32407  ssmd2  32408  atexch  32477  mdsymlem4  32502  sumdmdlem  32514  ifeqeqx  32637  fmptcof2  32756  padct  32817  nnindf  32919  drng0mxidl  33566  constr01  33933  pwsiga  34321  pwldsys  34348  ldsysgenld  34351  fiunelros  34365  breprexp  34824  bnj151  35066  bnj594  35101  bnj600  35108  trssfir1om  35299  trssfir1omregs  35324  subfacp1lem6  35420  erdszelem8  35433  cvmliftlem7  35526  cvmliftlem10  35529  cvmlift2lem12  35549  sat1el2xp  35614  mrsubfval  35743  msubfval  35759  mclsssvlem  35797  antnestlaw2  35927  funpartfv  36180  endofsegid  36320  broutsideof2  36357  a1i24  36536  nn0prpwlem  36557  nn0prpw  36558  ordcmp  36682  findreccl  36688  axtcond  36713  dfttc2g  36741  dfttc4lem2  36764  bj-cbvaw  36988  bj-cbveaw  36990  bj-ax6e  37015  bj-ax12v3ALT  37036  bj-xpnzex  37319  bj-ideqg1  37531  rdgssun  37747  finxp00  37771  domalom  37773  isinf2  37774  fvineqsneq  37781  wl-spae  37899  wl-nfs1t  37915  poimirlem27  38021  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  itg2addnclem3  38047  itg2addnc  38048  ftc1anc  38075  areacirclem1  38082  sdclem2  38116  fdc  38119  mettrifi  38131  isexid2  38229  zerdivemp1x  38321  smprngopr  38426  mpobi123f  38536  mptbi12f  38540  ac6s6  38546  relcnveq3  38701  mopickr  38745  elrelscnveq3  39001  disjlem14  39275  jca3  39355  ax12fromc15  39404  hbequid  39408  dvelimf-o  39428  ax12eq  39440  ax12el  39441  ax12indalem  39444  ax12inda2ALT  39445  ax12inda2  39446  lfl1dim  39620  lfl1dim2N  39621  lkreqN  39669  cvrexchlem  39918  ps-2  39977  paddasslem14  40332  idldil  40613  isltrn2N  40619  cdleme25a  40852  dibglbN  41665  dihlsscpre  41733  dvh4dimlem  41942  lcfl7N  42000  mapdval2N  42129  dvrelog2b  42558  aks6d1c6lem3  42664  monotoddzzfi  43394  onov0suclim  43726  onmcl  43783  omabs2  43784  tfsconcat0b  43798  naddgeoa  43846  rp-fakeimass  43963  clublem  44061  grur1cld  44683  ee121  44956  ee122  44957  rspsbc2  44985  ax6e2ndeq  45010  vd12  45051  vd13  45052  ee221  45101  ee212  45103  ee112  45106  ee211  45109  ee210  45111  ee201  45113  ee120  45115  ee021  45117  ee012  45119  ee102  45121  ee03  45191  ee31  45202  ee31an  45204  ee123  45213  ax6e2ndeqVD  45359  ax6e2ndeqALT  45381  refsum2cnlem1  45492  fiiuncl  45520  eliin2f  45558  disjrnmpt2  45642  disjinfi  45646  rnmptbdlem  45706  allbutfi  45844  infxrunb3rnmpt  45878  infrpgernmpt  45915  monoordxrv  45931  mccl  46050  constlimc  46076  limclner  46101  xlimmnfvlem1  46282  xlimpnfvlem1  46286  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnprodlem3  46398  stoweidlem31  46481  pwsal  46765  prsal  46768  sge0pnffigt  46846  sge0ltfirp  46850  0ome  46979  hoicvrrex  47006  hoidmvle  47050  ovnhoilem1  47051  ovnlecvr2  47060  smflimlem3  47223  ormkglobd  47327  chnsubseqword  47330  funressnfv  47513  euoreqb  47579  ndmaovass  47676  afv2orxorb  47698  otiunsndisjX  47749  nltle2tri  47783  nnmul2b  47801  m1modmmod  47834  smonoord  47847  iccpartigtl  47905  icceuelpartlem  47917  iccpartnel  47920  sprsymrelfolem2  47975  prproropf1olem4  47988  paireqne  47993  reupr  48004  reuopreuprim  48008  nprmmul3  48011  fmtnoprmfac1  48050  fmtnoprmfac2  48052  prmdvdsfmtnof1lem2  48070  31prm  48082  lighneallem3  48092  lighneallem4b  48094  lighneallem4  48095  lighneal  48096  nprmdvdsfacm1lem2  48106  ppivalnnnprm  48113  nn0o1gt2ALTV  48192  nn0oALTV  48194  odd2prm2  48216  even3prm2  48217  fpprwppr  48237  stgoldbwt  48274  sbgoldbwt  48275  sbgoldbalt  48279  sbgoldbo  48285  nnsum3primesgbe  48290  wtgoldbnnsum4prm  48300  bgoldbnnsum3prm  48302  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  bgoldbtbndlem4  48306  bgoldbtbnd  48307  bgoldbachlt  48311  tgblthelfgott  48313  dfclnbgr6  48354  grimco  48387  uhgrimisgrgric  48429  grtriprop  48439  usgrgrtrirex  48448  isubgr3stgrlem6  48469  isubgr3stgrlem8  48471  grlimprclnbgr  48494  grlimgrtri  48501  gpgedg2ov  48564  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpgcubic  48577  gpg5nbgr3star  48579  gpgprismgr4cycllem7  48599  pgnbgreunbgrlem2  48615  gpg5edgnedg  48628  upgrwlkupwlk  48638  rngccatidALTV  48770  ringccatidALTV  48804  lincdifsn  48922  lindslinindimp2lem1  48956  lindsrng01  48966  ldepsnlinc  49006  blen1b  49086  nn0sumshdiglemB  49118  nn0sumshdiglem1  49119  reorelicc  49208  rrx2xpref1o  49216  rrx2plord2  49220  rrxlinesc  49233  line2ylem  49249  line2xlem  49251  thincmon  49930  thincepi  49931