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  2427  ax12vALT  2473  nfsb4t  2503  moexexlem  2626  pm2.61da3ne  3021  ralrimivw  3133  rexlimdvw  3143  reximdv  3152  vtocl2d  3507  reuind  3699  reuan  3834  2reu4  4464  rabeqsnd  4613  tppreqb  4750  ssprsseq  4768  n0snor2el  4776  prnebg  4799  prel12g  4807  elpreqprlem  4809  3elpr2eq  4849  disjord  5074  disjiund  5076  dtruALT2  5312  exneq  5388  propssopi  5462  opthhausdorff  5471  fr0  5609  ssrel2  5741  poltletr  6095  reuop  6257  ordsssuc2  6416  ordnbtwn  6418  ndmfv  6872  fveqres  6884  fmptco  7082  funsndifnop  7105  tpres  7156  fntpb  7164  elunirn  7206  isof1oopb  7280  ndmovord  7557  ordsucelsuc  7773  tfinds  7811  tfindsg  7812  limomss  7822  findsg  7848  finds1  7850  xpexr  7869  resf1extb  7885  bropopvvv  8040  bropfvvvvlem  8041  bropfvvvv  8042  soxp  8079  poseq  8108  suppun  8134  extmptsuppeq  8138  funsssuppss  8140  suppss  8144  suppss2  8150  suppssfv  8152  suppco  8156  mpoxopynvov0  8168  smofvon2  8296  oaordi  8481  oawordeulem  8489  odi  8514  omeulem1  8517  brdomg  8905  snmapen  8985  fopwdom  9023  fodomr  9066  mapxpen  9081  infensuc  9093  fineqvlem  9176  fineqv  9177  fodomfir  9238  finsschain  9269  fsuppun  9300  fsuppunbi  9302  funsnfsupp  9305  dffi3  9344  fisup2g  9382  fisupcl  9383  fiinf2g  9415  infsupprpr  9419  wemapso2  9468  epnsym  9530  en3lplem2  9534  preleqg  9536  inf3lemd  9548  r1ordg  9702  r1val1  9710  r1pw  9769  r1pwALT  9770  rankxplim3  9805  eldju2ndl  9848  eldju2ndr  9849  carddomi2  9894  fidomtri  9917  alephon  9991  alephcard  9992  alephnbtwn  9993  alephordi  9996  iunfictbso  10036  fin23lem30  10264  fin1a2lem10  10331  axdc3lem2  10373  axdc3lem4  10375  alephval2  10495  cfpwsdom  10507  axextnd  10514  axrepnd  10517  axpownd  10524  axregnd  10527  axinfndlem1  10528  fpwwe2lem11  10564  wunfi  10644  addnidpi  10824  pinq  10850  mulgt0sr  11028  dedekind  11309  indval0  12163  nnind  12192  nn1m1nn  12195  nn0n0n1ge2b  12506  nn0lt2  12592  nn0le2is012  12593  uzm1  12822  uzinfi  12878  nn01to3  12891  xrltnsym  13088  xrlttri  13090  xrlttr  13091  qbtwnxr  13152  xltnegi  13168  xnn0xaddcl  13187  xlt2add  13212  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  reltxrnmnf  13295  fzdif1  13559  fzospliti  13646  elfzonlteqm1  13696  fzoopth  13717  elfznelfzo  13728  injresinjlem  13745  injresinj  13746  modfzo0difsn  13905  addmodlteq  13908  ssnn0fi  13947  fsuppmapnn0fiub0  13955  suppssfz  13956  seqfveq2  13986  monoord  13994  seqf1o  14005  seqhomo  14011  expnngt1  14203  faclbnd4lem4  14258  hasheqf1oi  14313  hashrabsn1  14336  hashgt0elex  14363  hash1snb  14381  hashf1lem2  14418  hashf1  14419  seqcoll  14426  hashle2pr  14439  pr2pwpr  14441  hashge2el2difr  14443  swrdnnn0nd  14619  swrdnd0  14620  pfxnd0  14651  swrdswrd  14667  pfxccatin12lem3  14694  pfxccat3  14696  swrdccat3blem  14701  repsdf2  14740  repswsymballbi  14742  cshw0  14756  cshwmodn  14757  cshwn  14759  cshwcl  14760  cshwlen  14761  cshw1  14784  2cshwcshw  14787  cshimadifsn  14791  s3sndisj  14929  s3iunsndisj  14930  relexprelg  15000  relexpnndm  15003  relexpaddg  15015  relexpaddd  15016  rtrclreclem4  15023  relexpindlem  15025  rexuz3  15311  rexanuz2  15312  limsupgre  15443  rlimconst  15506  caurcvg  15639  caucvg  15641  sumss  15686  fsumcl2lem  15693  modfsummods  15756  fsumrlim  15774  fsumo1  15775  fprodcl2lem  15915  dvdsaddre2b  16276  dvdsabseq  16282  mod2eq1n2dvds  16316  nno  16351  sumeven  16356  sumodd  16357  nn0rppwr  16530  nn0seqcvgd  16539  lcmdvds  16577  lcmfunsnlem2  16609  lcmfunsnlem  16610  divgcdcoprm0  16634  ge2nprmge4  16671  exprmfct  16674  rpexp1i  16693  prm23lt5  16785  prm23ge5  16786  pcz  16852  pcadd  16860  pcmptcl  16862  oddprmdvds  16874  prmgaplem6  17027  prmgaplem7  17028  cshwshashlem1  17066  cshwsdisj  17069  prmlem0  17076  setsstruct  17146  ressress  17217  initoeu2lem2  17982  mgm2nsgrplem2  18890  mgm2nsgrplem3  18891  dfgrp2e  18939  dfgrp3e  19016  cyccom  19178  symgextf1  19396  gsmsymgrfix  19403  gsmsymgreq  19407  sylow1lem1  19573  efgsf  19704  efgrelexlema  19724  dprdss  20006  ablfac1eulem  20049  01eq0ringOLD  20508  nrhmzr  20514  funcrngcsetcALT  20618  lssssr  20949  psgnodpm  21568  psrvscafval  21927  mplcoe1  22015  mplcoe5  22018  mpfrcl  22063  mamudm  22360  matmulcell  22410  dmatmul  22462  scmatsgrp1  22487  mavmuldm  22515  mavmulsolcl  22516  mdetunilem9  22585  cramerlem3  22654  cramer0  22655  chpscmatgsumbin  22809  chp0mat  22811  fvmptnn04ifc  22817  fvmptnn04ifd  22818  epttop  22974  neiptopnei  23097  fiuncmp  23369  1stcrest  23418  kgenss  23508  hmeofval  23723  fbun  23805  fgss2  23839  filuni  23850  filssufilg  23876  filufint  23885  hausflimi  23945  hausflim  23946  hauspwpwf1  23952  fclscmp  23995  alexsubALTlem4  24015  ptcmplem3  24019  ptcmplem5  24021  cstucnd  24248  isxmet2d  24292  imasdsf1olem  24338  blfps  24371  blf  24372  metrest  24489  nrginvrcn  24657  nmoge0  24686  nmoleub  24696  fsumcn  24837  cmetcaulem  25255  iscmet3  25260  iscmet2  25261  bcthlem2  25292  ovolicc2lem3  25486  itg2seq  25709  itg2splitlem  25715  itgeq1fOLD  25739  itgeq2  25745  iblcnlem  25756  itgfsum  25794  limcnlp  25845  perfdvf  25870  dvnres  25898  dvmptfsum  25942  c1lip1  25964  dvply2g  26251  taylply2  26333  abelth  26406  cxpsqrtth  26694  rlimcnp  26929  xrlimcnp  26932  jensen  26952  ppiublem1  27165  dchrelbas3  27201  bcmono  27240  zabsle1  27259  gausslemma2dlem0f  27324  gausslemma2dlem1a  27328  gausslemma2dlem4  27332  lgsquad2lem2  27348  2lgslem1a1  27352  2lgslem3  27367  2lgs  27370  2lgsoddprm  27379  2sqlem10  27391  2sqnn  27402  addsqnreup  27406  2sqreultblem  27411  2sqreunnltblem  27414  pntrsumbnd2  27530  pntpbnd1  27549  pntlem3  27572  nolesgn2o  27635  noetalem1  27705  bday0b  27805  leftf  27847  rightf  27848  oldss  27862  addcutslem  27969  negcut  28031  mulcutlem  28123  n0s0suc  28334  n0fincut  28347  n0s0m1  28354  nn1m1nns  28366  axcontlem7  29039  elntg2  29054  ausgrusgrb  29234  usgredg2v  29296  lfuhgr1v0e  29323  subumgredg2  29354  upgrreslem  29373  umgrreslem  29374  fusgrfisbase  29397  nbuhgr  29412  uhgrnbgr0nb  29423  nbgr0edglem  29425  nbgr1vtx  29427  cusgredg  29493  cusgrsizeinds  29521  sizusglecusg  29532  finsumvtxdg2size  29619  ewlkle  29674  upgriswlk  29709  pthdivtx  29795  dfpth2  29797  usgr2trlncl  29828  crctcshwlkn0lem4  29881  wwlksn  29905  iswwlksnon  29921  iswspthsnon  29924  wwlksm1edg  29949  wwlksnfi  29974  2pthdlem1  29998  umgr2wlk  30017  umgrclwwlkge2  30061  clwlkclwwlklem2a  30068  clwlkclwwlk  30072  clwlkclwwlkf1lem2  30075  clwlkclwwlkf  30078  clwwisshclwws  30085  clwwlknlbonbgr1  30109  clwwlknon0  30163  clwwlknonel  30165  clwwlknonex2e  30180  3pthdlem1  30234  eupth2  30309  nfrgr2v  30342  frgr3vlem1  30343  1to2vfriswmgr  30349  1to3vfriswmgr  30350  vdgn1frgrv2  30366  frgrncvvdeqlem9  30377  frgrwopreglem4a  30380  frgrregorufr0  30394  frgrregorufr  30395  2wspmdisj  30407  2clwwlk2clwwlklem  30416  frgrreggt1  30463  frgrreg  30464  frgrregord13  30466  aevdemo  30530  shsvs  31394  0cnop  32050  0cnfn  32051  cnlnssadj  32151  ssmd1  32382  ssmd2  32383  atexch  32452  mdsymlem4  32477  sumdmdlem  32489  ifeqeqx  32612  fmptcof2  32730  padct  32791  nnindf  32893  drng0mxidl  33536  constr01  33886  pwsiga  34274  pwldsys  34301  ldsysgenld  34304  fiunelros  34318  breprexp  34777  bnj151  35019  bnj594  35054  bnj600  35061  trssfir1om  35255  trssfir1omregs  35280  subfacp1lem6  35367  erdszelem8  35380  cvmliftlem7  35473  cvmliftlem10  35476  cvmlift2lem12  35496  sat1el2xp  35561  mrsubfval  35690  msubfval  35706  mclsssvlem  35744  antnestlaw2  35874  funpartfv  36127  endofsegid  36267  broutsideof2  36304  a1i24  36483  nn0prpwlem  36504  nn0prpw  36505  ordcmp  36629  findreccl  36635  axtcond  36660  dfttc2g  36688  dfttc4lem2  36711  bj-cbvaw  36935  bj-cbveaw  36937  bj-ax6e  36962  bj-ax12v3ALT  36983  bj-xpnzex  37266  bj-ideqg1  37478  rdgssun  37694  finxp00  37718  domalom  37720  isinf2  37721  fvineqsneq  37728  wl-spae  37846  wl-nfs1t  37862  poimirlem27  37968  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  itg2addnclem3  37994  itg2addnc  37995  ftc1anc  38022  areacirclem1  38029  sdclem2  38063  fdc  38066  mettrifi  38078  isexid2  38176  zerdivemp1x  38268  smprngopr  38373  mpobi123f  38483  mptbi12f  38487  ac6s6  38493  relcnveq3  38648  mopickr  38692  elrelscnveq3  38948  disjlem14  39222  jca3  39302  ax12fromc15  39351  hbequid  39355  dvelimf-o  39375  ax12eq  39387  ax12el  39388  ax12indalem  39391  ax12inda2ALT  39392  ax12inda2  39393  lfl1dim  39567  lfl1dim2N  39568  lkreqN  39616  cvrexchlem  39865  ps-2  39924  paddasslem14  40279  idldil  40560  isltrn2N  40566  cdleme25a  40799  dibglbN  41612  dihlsscpre  41680  dvh4dimlem  41889  lcfl7N  41947  mapdval2N  42076  dvrelog2b  42505  aks6d1c6lem3  42611  monotoddzzfi  43370  onov0suclim  43702  onmcl  43759  omabs2  43760  tfsconcat0b  43774  naddgeoa  43822  rp-fakeimass  43939  clublem  44037  grur1cld  44659  ee121  44932  ee122  44933  rspsbc2  44961  ax6e2ndeq  44986  vd12  45027  vd13  45028  ee221  45077  ee212  45079  ee112  45082  ee211  45085  ee210  45087  ee201  45089  ee120  45091  ee021  45093  ee012  45095  ee102  45097  ee03  45167  ee31  45178  ee31an  45180  ee123  45189  ax6e2ndeqVD  45335  ax6e2ndeqALT  45357  refsum2cnlem1  45468  fiiuncl  45496  eliin2f  45534  disjrnmpt2  45618  disjinfi  45622  rnmptbdlem  45684  allbutfi  45822  infxrunb3rnmpt  45856  infrpgernmpt  45893  monoordxrv  45909  mccl  46028  constlimc  46054  limclner  46079  xlimmnfvlem1  46260  xlimpnfvlem1  46264  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnprodlem3  46376  stoweidlem31  46459  pwsal  46743  prsal  46746  sge0pnffigt  46824  sge0ltfirp  46828  0ome  46957  hoicvrrex  46984  hoidmvle  47028  ovnhoilem1  47029  ovnlecvr2  47038  smflimlem3  47201  ormkglobd  47305  chnsubseqword  47308  funressnfv  47491  euoreqb  47557  ndmaovass  47654  afv2orxorb  47676  otiunsndisjX  47727  nltle2tri  47761  nnmul2b  47779  m1modmmod  47812  smonoord  47825  iccpartigtl  47883  icceuelpartlem  47895  iccpartnel  47898  sprsymrelfolem2  47953  prproropf1olem4  47966  paireqne  47971  reupr  47982  reuopreuprim  47986  nprmmul3  47989  fmtnoprmfac1  48028  fmtnoprmfac2  48030  prmdvdsfmtnof1lem2  48048  31prm  48060  lighneallem3  48070  lighneallem4b  48072  lighneallem4  48073  lighneal  48074  nprmdvdsfacm1lem2  48084  ppivalnnnprm  48091  nn0o1gt2ALTV  48170  nn0oALTV  48172  odd2prm2  48194  even3prm2  48195  fpprwppr  48215  stgoldbwt  48252  sbgoldbwt  48253  sbgoldbalt  48257  sbgoldbo  48263  nnsum3primesgbe  48268  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  bgoldbachlt  48289  tgblthelfgott  48291  dfclnbgr6  48332  grimco  48365  uhgrimisgrgric  48407  grtriprop  48417  usgrgrtrirex  48426  isubgr3stgrlem6  48447  isubgr3stgrlem8  48449  grlimprclnbgr  48472  grlimgrtri  48479  gpgedg2ov  48542  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpgcubic  48555  gpg5nbgr3star  48557  gpgprismgr4cycllem7  48577  pgnbgreunbgrlem2  48593  gpg5edgnedg  48606  upgrwlkupwlk  48616  rngccatidALTV  48748  ringccatidALTV  48782  lincdifsn  48900  lindslinindimp2lem1  48934  lindsrng01  48944  ldepsnlinc  48984  blen1b  49064  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  reorelicc  49186  rrx2xpref1o  49194  rrx2plord2  49198  rrxlinesc  49211  line2ylem  49227  line2xlem  49229  thincmon  49908  thincepi  49909