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  185  mtod  198  imbi2d  340  adantr  480  jctild  525  jctird  526  anbi2d  631  anbi1d  632  pm3.4  810  impsingle  1629  meredith  1643  stdpc4  2074  ax12  2428  ax12vALT  2474  nfsb4t  2504  moexexlem  2627  pm2.61da3ne  3022  ralrimivw  3134  rexlimdvw  3144  reximdv  3153  vtocl2d  3508  reuind  3700  reuan  3835  2reu4  4465  rabeqsnd  4614  tppreqb  4749  ssprsseq  4769  n0snor2el  4777  prnebg  4800  prel12g  4808  elpreqprlem  4810  3elpr2eq  4850  disjord  5075  disjiund  5077  dtruALT2  5307  exneq  5383  propssopi  5456  opthhausdorff  5465  fr0  5602  ssrel2  5734  poltletr  6089  reuop  6251  ordsssuc2  6410  ordnbtwn  6412  ndmfv  6866  fveqres  6878  fmptco  7076  funsndifnop  7098  tpres  7149  fntpb  7157  elunirn  7199  isof1oopb  7273  ndmovord  7550  ordsucelsuc  7766  tfinds  7804  tfindsg  7805  limomss  7815  findsg  7841  finds1  7843  xpexr  7862  resf1extb  7878  bropopvvv  8033  bropfvvvvlem  8034  bropfvvvv  8035  soxp  8072  poseq  8101  suppun  8127  extmptsuppeq  8131  funsssuppss  8133  suppss  8137  suppss2  8143  suppssfv  8145  suppco  8149  mpoxopynvov0  8161  smofvon2  8289  oaordi  8474  oawordeulem  8482  odi  8507  omeulem1  8510  brdomg  8898  snmapen  8978  fopwdom  9016  fodomr  9059  mapxpen  9074  infensuc  9086  fineqvlem  9169  fineqv  9170  fodomfir  9231  finsschain  9262  fsuppun  9293  fsuppunbi  9295  funsnfsupp  9298  dffi3  9337  fisup2g  9375  fisupcl  9376  fiinf2g  9408  infsupprpr  9412  wemapso2  9461  epnsym  9521  en3lplem2  9525  preleqg  9527  inf3lemd  9539  r1ordg  9693  r1val1  9701  r1pw  9760  r1pwALT  9761  rankxplim3  9796  eldju2ndl  9839  eldju2ndr  9840  carddomi2  9885  fidomtri  9908  alephon  9982  alephcard  9983  alephnbtwn  9984  alephordi  9987  iunfictbso  10027  fin23lem30  10255  fin1a2lem10  10322  axdc3lem2  10364  axdc3lem4  10366  alephval2  10486  cfpwsdom  10498  axextnd  10505  axrepnd  10508  axpownd  10515  axregnd  10518  axinfndlem1  10519  fpwwe2lem11  10555  wunfi  10635  addnidpi  10815  pinq  10841  mulgt0sr  11019  dedekind  11300  indval0  12154  nnind  12183  nn1m1nn  12186  nn0n0n1ge2b  12497  nn0lt2  12583  nn0le2is012  12584  uzm1  12813  uzinfi  12869  nn01to3  12882  xrltnsym  13079  xrlttri  13081  xrlttr  13082  qbtwnxr  13143  xltnegi  13159  xnn0xaddcl  13178  xlt2add  13203  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  reltxrnmnf  13286  fzdif1  13550  fzospliti  13637  elfzonlteqm1  13687  fzoopth  13708  elfznelfzo  13719  injresinjlem  13736  injresinj  13737  modfzo0difsn  13896  addmodlteq  13899  ssnn0fi  13938  fsuppmapnn0fiub0  13946  suppssfz  13947  seqfveq2  13977  monoord  13985  seqf1o  13996  seqhomo  14002  expnngt1  14194  faclbnd4lem4  14249  hasheqf1oi  14304  hashrabsn1  14327  hashgt0elex  14354  hash1snb  14372  hashf1lem2  14409  hashf1  14410  seqcoll  14417  hashle2pr  14430  pr2pwpr  14432  hashge2el2difr  14434  swrdnnn0nd  14610  swrdnd0  14611  pfxnd0  14642  swrdswrd  14658  pfxccatin12lem3  14685  pfxccat3  14687  swrdccat3blem  14692  repsdf2  14731  repswsymballbi  14733  cshw0  14747  cshwmodn  14748  cshwn  14750  cshwcl  14751  cshwlen  14752  cshw1  14775  2cshwcshw  14778  cshimadifsn  14782  s3sndisj  14920  s3iunsndisj  14921  relexprelg  14991  relexpnndm  14994  relexpaddg  15006  relexpaddd  15007  rtrclreclem4  15014  relexpindlem  15016  rexuz3  15302  rexanuz2  15303  limsupgre  15434  rlimconst  15497  caurcvg  15630  caucvg  15632  sumss  15677  fsumcl2lem  15684  modfsummods  15747  fsumrlim  15765  fsumo1  15766  fprodcl2lem  15906  dvdsaddre2b  16267  dvdsabseq  16273  mod2eq1n2dvds  16307  nno  16342  sumeven  16347  sumodd  16348  nn0rppwr  16521  nn0seqcvgd  16530  lcmdvds  16568  lcmfunsnlem2  16600  lcmfunsnlem  16601  divgcdcoprm0  16625  ge2nprmge4  16662  exprmfct  16665  rpexp1i  16684  prm23lt5  16776  prm23ge5  16777  pcz  16843  pcadd  16851  pcmptcl  16853  oddprmdvds  16865  prmgaplem6  17018  prmgaplem7  17019  cshwshashlem1  17057  cshwsdisj  17060  prmlem0  17067  setsstruct  17137  ressress  17208  initoeu2lem2  17973  mgm2nsgrplem2  18881  mgm2nsgrplem3  18882  dfgrp2e  18930  dfgrp3e  19007  cyccom  19169  symgextf1  19387  gsmsymgrfix  19394  gsmsymgreq  19398  sylow1lem1  19564  efgsf  19695  efgrelexlema  19715  dprdss  19997  ablfac1eulem  20040  01eq0ringOLD  20499  nrhmzr  20505  funcrngcsetcALT  20609  lssssr  20940  psgnodpm  21578  psrvscafval  21937  mplcoe1  22025  mplcoe5  22028  mpfrcl  22073  mamudm  22370  matmulcell  22420  dmatmul  22472  scmatsgrp1  22497  mavmuldm  22525  mavmulsolcl  22526  mdetunilem9  22595  cramerlem3  22664  cramer0  22665  chpscmatgsumbin  22819  chp0mat  22821  fvmptnn04ifc  22827  fvmptnn04ifd  22828  epttop  22984  neiptopnei  23107  fiuncmp  23379  1stcrest  23428  kgenss  23518  hmeofval  23733  fbun  23815  fgss2  23849  filuni  23860  filssufilg  23886  filufint  23895  hausflimi  23955  hausflim  23956  hauspwpwf1  23962  fclscmp  24005  alexsubALTlem4  24025  ptcmplem3  24029  ptcmplem5  24031  cstucnd  24258  isxmet2d  24302  imasdsf1olem  24348  blfps  24381  blf  24382  metrest  24499  nrginvrcn  24667  nmoge0  24696  nmoleub  24706  fsumcn  24847  cmetcaulem  25265  iscmet3  25270  iscmet2  25271  bcthlem2  25302  ovolicc2lem3  25496  itg2seq  25719  itg2splitlem  25725  itgeq1fOLD  25749  itgeq2  25755  iblcnlem  25766  itgfsum  25804  limcnlp  25855  perfdvf  25880  dvnres  25908  dvmptfsum  25952  c1lip1  25974  dvply2g  26261  taylply2  26344  abelth  26419  cxpsqrtth  26707  rlimcnp  26942  xrlimcnp  26945  jensen  26966  ppiublem1  27179  dchrelbas3  27215  bcmono  27254  zabsle1  27273  gausslemma2dlem0f  27338  gausslemma2dlem1a  27342  gausslemma2dlem4  27346  lgsquad2lem2  27362  2lgslem1a1  27366  2lgslem3  27381  2lgs  27384  2lgsoddprm  27393  2sqlem10  27405  2sqnn  27416  addsqnreup  27420  2sqreultblem  27425  2sqreunnltblem  27428  pntrsumbnd2  27544  pntpbnd1  27563  pntlem3  27586  nolesgn2o  27649  noetalem1  27719  bday0b  27819  leftf  27861  rightf  27862  oldss  27876  addcutslem  27983  negcut  28045  mulcutlem  28137  n0s0suc  28348  n0fincut  28361  n0s0m1  28368  nn1m1nns  28380  axcontlem7  29053  elntg2  29068  ausgrusgrb  29248  usgredg2v  29310  lfuhgr1v0e  29337  subumgredg2  29368  upgrreslem  29387  umgrreslem  29388  fusgrfisbase  29411  nbuhgr  29426  uhgrnbgr0nb  29437  nbgr0edglem  29439  nbgr1vtx  29441  cusgredg  29507  cusgrsizeinds  29536  sizusglecusg  29547  finsumvtxdg2size  29634  ewlkle  29689  upgriswlk  29724  pthdivtx  29810  dfpth2  29812  usgr2trlncl  29843  crctcshwlkn0lem4  29896  wwlksn  29920  iswwlksnon  29936  iswspthsnon  29939  wwlksm1edg  29964  wwlksnfi  29989  2pthdlem1  30013  umgr2wlk  30032  umgrclwwlkge2  30076  clwlkclwwlklem2a  30083  clwlkclwwlk  30087  clwlkclwwlkf1lem2  30090  clwlkclwwlkf  30093  clwwisshclwws  30100  clwwlknlbonbgr1  30124  clwwlknon0  30178  clwwlknonel  30180  clwwlknonex2e  30195  3pthdlem1  30249  eupth2  30324  nfrgr2v  30357  frgr3vlem1  30358  1to2vfriswmgr  30364  1to3vfriswmgr  30365  vdgn1frgrv2  30381  frgrncvvdeqlem9  30392  frgrwopreglem4a  30395  frgrregorufr0  30409  frgrregorufr  30410  2wspmdisj  30422  2clwwlk2clwwlklem  30431  frgrreggt1  30478  frgrreg  30479  frgrregord13  30481  aevdemo  30545  shsvs  31409  0cnop  32065  0cnfn  32066  cnlnssadj  32166  ssmd1  32397  ssmd2  32398  atexch  32467  mdsymlem4  32492  sumdmdlem  32504  ifeqeqx  32627  fmptcof2  32745  padct  32806  nnindf  32908  drng0mxidl  33551  constr01  33902  pwsiga  34290  pwldsys  34317  ldsysgenld  34320  fiunelros  34334  breprexp  34793  bnj151  35035  bnj594  35070  bnj600  35077  trssfir1om  35271  trssfir1omregs  35296  subfacp1lem6  35383  erdszelem8  35396  cvmliftlem7  35489  cvmliftlem10  35492  cvmlift2lem12  35512  sat1el2xp  35577  mrsubfval  35706  msubfval  35722  mclsssvlem  35760  antnestlaw2  35890  funpartfv  36143  endofsegid  36283  broutsideof2  36320  a1i24  36499  nn0prpwlem  36520  nn0prpw  36521  ordcmp  36645  findreccl  36651  axtcond  36676  dfttc2g  36704  dfttc4lem2  36727  bj-cbvaw  36951  bj-cbveaw  36953  bj-ax6e  36978  bj-ax12v3ALT  36999  bj-xpnzex  37282  bj-ideqg1  37494  rdgssun  37708  finxp00  37732  domalom  37734  isinf2  37735  fvineqsneq  37742  wl-spae  37860  wl-nfs1t  37876  poimirlem27  37982  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  itg2addnclem3  38008  itg2addnc  38009  ftc1anc  38036  areacirclem1  38043  sdclem2  38077  fdc  38080  mettrifi  38092  isexid2  38190  zerdivemp1x  38282  smprngopr  38387  mpobi123f  38497  mptbi12f  38501  ac6s6  38507  relcnveq3  38662  mopickr  38706  elrelscnveq3  38962  disjlem14  39236  jca3  39316  ax12fromc15  39365  hbequid  39369  dvelimf-o  39389  ax12eq  39401  ax12el  39402  ax12indalem  39405  ax12inda2ALT  39406  ax12inda2  39407  lfl1dim  39581  lfl1dim2N  39582  lkreqN  39630  cvrexchlem  39879  ps-2  39938  paddasslem14  40293  idldil  40574  isltrn2N  40580  cdleme25a  40813  dibglbN  41626  dihlsscpre  41694  dvh4dimlem  41903  lcfl7N  41961  mapdval2N  42090  dvrelog2b  42519  aks6d1c6lem3  42625  monotoddzzfi  43388  onov0suclim  43720  onmcl  43777  omabs2  43778  tfsconcat0b  43792  naddgeoa  43840  rp-fakeimass  43957  clublem  44055  grur1cld  44677  ee121  44950  ee122  44951  rspsbc2  44979  ax6e2ndeq  45004  vd12  45045  vd13  45046  ee221  45095  ee212  45097  ee112  45100  ee211  45103  ee210  45105  ee201  45107  ee120  45109  ee021  45111  ee012  45113  ee102  45115  ee03  45185  ee31  45196  ee31an  45198  ee123  45207  ax6e2ndeqVD  45353  ax6e2ndeqALT  45375  refsum2cnlem1  45486  fiiuncl  45514  eliin2f  45552  disjrnmpt2  45636  disjinfi  45640  rnmptbdlem  45702  allbutfi  45840  infxrunb3rnmpt  45874  infrpgernmpt  45911  monoordxrv  45927  mccl  46046  constlimc  46072  limclner  46097  xlimmnfvlem1  46278  xlimpnfvlem1  46282  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnprodlem3  46394  stoweidlem31  46477  pwsal  46761  prsal  46764  sge0pnffigt  46842  sge0ltfirp  46846  0ome  46975  hoicvrrex  47002  hoidmvle  47046  ovnhoilem1  47047  ovnlecvr2  47056  smflimlem3  47219  ormkglobd  47321  chnsubseqword  47324  funressnfv  47503  euoreqb  47569  ndmaovass  47666  afv2orxorb  47688  otiunsndisjX  47739  nltle2tri  47773  nnmul2b  47791  m1modmmod  47824  smonoord  47837  iccpartigtl  47895  icceuelpartlem  47907  iccpartnel  47910  sprsymrelfolem2  47965  prproropf1olem4  47978  paireqne  47983  reupr  47994  reuopreuprim  47998  nprmmul3  48001  fmtnoprmfac1  48040  fmtnoprmfac2  48042  prmdvdsfmtnof1lem2  48060  31prm  48072  lighneallem3  48082  lighneallem4b  48084  lighneallem4  48085  lighneal  48086  nprmdvdsfacm1lem2  48096  ppivalnnnprm  48103  nn0o1gt2ALTV  48182  nn0oALTV  48184  odd2prm2  48206  even3prm2  48207  fpprwppr  48227  stgoldbwt  48264  sbgoldbwt  48265  sbgoldbalt  48269  sbgoldbo  48275  nnsum3primesgbe  48280  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbndlem4  48296  bgoldbtbnd  48297  bgoldbachlt  48301  tgblthelfgott  48303  dfclnbgr6  48344  grimco  48377  uhgrimisgrgric  48419  grtriprop  48429  usgrgrtrirex  48438  isubgr3stgrlem6  48459  isubgr3stgrlem8  48461  grlimprclnbgr  48484  grlimgrtri  48491  gpgedg2ov  48554  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpgcubic  48567  gpg5nbgr3star  48569  gpgprismgr4cycllem7  48589  pgnbgreunbgrlem2  48605  gpg5edgnedg  48618  upgrwlkupwlk  48628  rngccatidALTV  48760  ringccatidALTV  48794  lincdifsn  48912  lindslinindimp2lem1  48946  lindsrng01  48956  ldepsnlinc  48996  blen1b  49076  nn0sumshdiglemB  49108  nn0sumshdiglem1  49109  reorelicc  49198  rrx2xpref1o  49206  rrx2plord2  49210  rrxlinesc  49223  line2ylem  49239  line2xlem  49241  thincmon  49920  thincepi  49921