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  5305  exneq  5381  propssopi  5454  opthhausdorff  5463  fr0  5600  ssrel2  5732  poltletr  6087  reuop  6249  ordsssuc2  6408  ordnbtwn  6410  ndmfv  6864  fveqres  6876  fmptco  7074  funsndifnop  7096  tpres  7147  fntpb  7155  elunirn  7197  isof1oopb  7271  ndmovord  7548  ordsucelsuc  7764  tfinds  7802  tfindsg  7803  limomss  7813  findsg  7839  finds1  7841  xpexr  7860  resf1extb  7876  bropopvvv  8031  bropfvvvvlem  8032  bropfvvvv  8033  soxp  8070  poseq  8099  suppun  8125  extmptsuppeq  8129  funsssuppss  8131  suppss  8135  suppss2  8141  suppssfv  8143  suppco  8147  mpoxopynvov0  8159  smofvon2  8287  oaordi  8472  oawordeulem  8480  odi  8505  omeulem1  8508  brdomg  8896  snmapen  8976  fopwdom  9014  fodomr  9057  mapxpen  9072  infensuc  9084  fineqvlem  9167  fineqv  9168  fodomfir  9229  finsschain  9260  fsuppun  9291  fsuppunbi  9293  funsnfsupp  9296  dffi3  9335  fisup2g  9373  fisupcl  9374  fiinf2g  9406  infsupprpr  9410  wemapso2  9459  epnsym  9519  en3lplem2  9523  preleqg  9525  inf3lemd  9537  r1ordg  9691  r1val1  9699  r1pw  9758  r1pwALT  9759  rankxplim3  9794  eldju2ndl  9837  eldju2ndr  9838  carddomi2  9883  fidomtri  9906  alephon  9980  alephcard  9981  alephnbtwn  9982  alephordi  9985  iunfictbso  10025  fin23lem30  10253  fin1a2lem10  10320  axdc3lem2  10362  axdc3lem4  10364  alephval2  10484  cfpwsdom  10496  axextnd  10503  axrepnd  10506  axpownd  10513  axregnd  10516  axinfndlem1  10517  fpwwe2lem11  10553  wunfi  10633  addnidpi  10813  pinq  10839  mulgt0sr  11017  dedekind  11298  indval0  12152  nnind  12181  nn1m1nn  12184  nn0n0n1ge2b  12495  nn0lt2  12581  nn0le2is012  12582  uzm1  12811  uzinfi  12867  nn01to3  12880  xrltnsym  13077  xrlttri  13079  xrlttr  13080  qbtwnxr  13141  xltnegi  13157  xnn0xaddcl  13176  xlt2add  13201  xrsupsslem  13248  xrinfmsslem  13249  xrub  13253  reltxrnmnf  13284  fzdif1  13548  fzospliti  13635  elfzonlteqm1  13685  fzoopth  13706  elfznelfzo  13717  injresinjlem  13734  injresinj  13735  modfzo0difsn  13894  addmodlteq  13897  ssnn0fi  13936  fsuppmapnn0fiub0  13944  suppssfz  13945  seqfveq2  13975  monoord  13983  seqf1o  13994  seqhomo  14000  expnngt1  14192  faclbnd4lem4  14247  hasheqf1oi  14302  hashrabsn1  14325  hashgt0elex  14352  hash1snb  14370  hashf1lem2  14407  hashf1  14408  seqcoll  14415  hashle2pr  14428  pr2pwpr  14430  hashge2el2difr  14432  swrdnnn0nd  14608  swrdnd0  14609  pfxnd0  14640  swrdswrd  14656  pfxccatin12lem3  14683  pfxccat3  14685  swrdccat3blem  14690  repsdf2  14729  repswsymballbi  14731  cshw0  14745  cshwmodn  14746  cshwn  14748  cshwcl  14749  cshwlen  14750  cshw1  14773  2cshwcshw  14776  cshimadifsn  14780  s3sndisj  14918  s3iunsndisj  14919  relexprelg  14989  relexpnndm  14992  relexpaddg  15004  relexpaddd  15005  rtrclreclem4  15012  relexpindlem  15014  rexuz3  15300  rexanuz2  15301  limsupgre  15432  rlimconst  15495  caurcvg  15628  caucvg  15630  sumss  15675  fsumcl2lem  15682  modfsummods  15745  fsumrlim  15763  fsumo1  15764  fprodcl2lem  15904  dvdsaddre2b  16265  dvdsabseq  16271  mod2eq1n2dvds  16305  nno  16340  sumeven  16345  sumodd  16346  nn0rppwr  16519  nn0seqcvgd  16528  lcmdvds  16566  lcmfunsnlem2  16598  lcmfunsnlem  16599  divgcdcoprm0  16623  ge2nprmge4  16660  exprmfct  16663  rpexp1i  16682  prm23lt5  16774  prm23ge5  16775  pcz  16841  pcadd  16849  pcmptcl  16851  oddprmdvds  16863  prmgaplem6  17016  prmgaplem7  17017  cshwshashlem1  17055  cshwsdisj  17058  prmlem0  17065  setsstruct  17135  ressress  17206  initoeu2lem2  17971  mgm2nsgrplem2  18879  mgm2nsgrplem3  18880  dfgrp2e  18928  dfgrp3e  19005  cyccom  19167  symgextf1  19385  gsmsymgrfix  19392  gsmsymgreq  19396  sylow1lem1  19562  efgsf  19693  efgrelexlema  19713  dprdss  19995  ablfac1eulem  20038  01eq0ringOLD  20497  nrhmzr  20503  funcrngcsetcALT  20607  lssssr  20938  psgnodpm  21576  psrvscafval  21936  mplcoe1  22024  mplcoe5  22027  mpfrcl  22072  mamudm  22369  matmulcell  22419  dmatmul  22471  scmatsgrp1  22496  mavmuldm  22524  mavmulsolcl  22525  mdetunilem9  22594  cramerlem3  22663  cramer0  22664  chpscmatgsumbin  22818  chp0mat  22820  fvmptnn04ifc  22826  fvmptnn04ifd  22827  epttop  22983  neiptopnei  23106  fiuncmp  23378  1stcrest  23427  kgenss  23517  hmeofval  23732  fbun  23814  fgss2  23848  filuni  23859  filssufilg  23885  filufint  23894  hausflimi  23954  hausflim  23955  hauspwpwf1  23961  fclscmp  24004  alexsubALTlem4  24024  ptcmplem3  24028  ptcmplem5  24030  cstucnd  24257  isxmet2d  24301  imasdsf1olem  24347  blfps  24380  blf  24381  metrest  24498  nrginvrcn  24666  nmoge0  24695  nmoleub  24705  fsumcn  24846  cmetcaulem  25264  iscmet3  25269  iscmet2  25270  bcthlem2  25301  ovolicc2lem3  25495  itg2seq  25718  itg2splitlem  25724  itgeq1fOLD  25748  itgeq2  25754  iblcnlem  25765  itgfsum  25803  limcnlp  25854  perfdvf  25879  dvnres  25907  dvmptfsum  25951  c1lip1  25974  dvply2g  26263  taylply2  26346  abelth  26422  cxpsqrtth  26710  rlimcnp  26946  xrlimcnp  26949  jensen  26970  ppiublem1  27184  dchrelbas3  27220  bcmono  27259  zabsle1  27278  gausslemma2dlem0f  27343  gausslemma2dlem1a  27347  gausslemma2dlem4  27351  lgsquad2lem2  27367  2lgslem1a1  27371  2lgslem3  27386  2lgs  27389  2lgsoddprm  27398  2sqlem10  27410  2sqnn  27421  addsqnreup  27425  2sqreultblem  27430  2sqreunnltblem  27433  pntrsumbnd2  27549  pntpbnd1  27568  pntlem3  27591  nolesgn2o  27654  noetalem1  27724  bday0b  27824  leftf  27866  rightf  27867  oldss  27881  addcutslem  27988  negcut  28050  mulcutlem  28142  n0s0suc  28353  n0fincut  28366  n0s0m1  28373  nn1m1nns  28385  axcontlem7  29058  elntg2  29073  ausgrusgrb  29253  usgredg2v  29315  lfuhgr1v0e  29342  subumgredg2  29373  upgrreslem  29392  umgrreslem  29393  fusgrfisbase  29416  nbuhgr  29431  uhgrnbgr0nb  29442  nbgr0edglem  29444  nbgr1vtx  29446  cusgredg  29512  cusgrsizeinds  29541  sizusglecusg  29552  finsumvtxdg2size  29639  ewlkle  29694  upgriswlk  29729  pthdivtx  29815  dfpth2  29817  usgr2trlncl  29848  crctcshwlkn0lem4  29901  wwlksn  29925  iswwlksnon  29941  iswspthsnon  29944  wwlksm1edg  29969  wwlksnfi  29994  2pthdlem1  30018  umgr2wlk  30037  umgrclwwlkge2  30081  clwlkclwwlklem2a  30088  clwlkclwwlk  30092  clwlkclwwlkf1lem2  30095  clwlkclwwlkf  30098  clwwisshclwws  30105  clwwlknlbonbgr1  30129  clwwlknon0  30183  clwwlknonel  30185  clwwlknonex2e  30200  3pthdlem1  30254  eupth2  30329  nfrgr2v  30362  frgr3vlem1  30363  1to2vfriswmgr  30369  1to3vfriswmgr  30370  vdgn1frgrv2  30386  frgrncvvdeqlem9  30397  frgrwopreglem4a  30400  frgrregorufr0  30414  frgrregorufr  30415  2wspmdisj  30427  2clwwlk2clwwlklem  30436  frgrreggt1  30483  frgrreg  30484  frgrregord13  30486  aevdemo  30550  shsvs  31414  0cnop  32070  0cnfn  32071  cnlnssadj  32171  ssmd1  32402  ssmd2  32403  atexch  32472  mdsymlem4  32497  sumdmdlem  32509  ifeqeqx  32632  fmptcof2  32750  padct  32811  nnindf  32913  drng0mxidl  33556  constr01  33907  pwsiga  34295  pwldsys  34322  ldsysgenld  34325  fiunelros  34339  breprexp  34798  bnj151  35040  bnj594  35075  bnj600  35082  trssfir1om  35276  trssfir1omregs  35301  subfacp1lem6  35388  erdszelem8  35401  cvmliftlem7  35494  cvmliftlem10  35497  cvmlift2lem12  35517  sat1el2xp  35582  mrsubfval  35711  msubfval  35727  mclsssvlem  35765  antnestlaw2  35895  funpartfv  36148  endofsegid  36288  broutsideof2  36325  a1i24  36504  nn0prpwlem  36525  nn0prpw  36526  ordcmp  36650  findreccl  36656  axtcond  36681  dfttc2g  36709  dfttc4lem2  36732  bj-cbvaw  36948  bj-cbveaw  36950  bj-ax6e  36975  bj-ax12v3ALT  36996  bj-xpnzex  37279  bj-ideqg1  37491  rdgssun  37705  finxp00  37729  domalom  37731  isinf2  37732  fvineqsneq  37739  wl-spae  37857  wl-nfs1t  37873  poimirlem27  37979  ovoliunnfl  37994  voliunnfl  37996  volsupnfl  37997  itg2addnclem3  38005  itg2addnc  38006  ftc1anc  38033  areacirclem1  38040  sdclem2  38074  fdc  38077  mettrifi  38089  isexid2  38187  zerdivemp1x  38279  smprngopr  38384  mpobi123f  38494  mptbi12f  38498  ac6s6  38504  relcnveq3  38659  mopickr  38703  elrelscnveq3  38959  disjlem14  39233  jca3  39313  ax12fromc15  39362  hbequid  39366  dvelimf-o  39386  ax12eq  39398  ax12el  39399  ax12indalem  39402  ax12inda2ALT  39403  ax12inda2  39404  lfl1dim  39578  lfl1dim2N  39579  lkreqN  39627  cvrexchlem  39876  ps-2  39935  paddasslem14  40290  idldil  40571  isltrn2N  40577  cdleme25a  40810  dibglbN  41623  dihlsscpre  41691  dvh4dimlem  41900  lcfl7N  41958  mapdval2N  42087  dvrelog2b  42516  aks6d1c6lem3  42622  monotoddzzfi  43385  onov0suclim  43717  onmcl  43774  omabs2  43775  tfsconcat0b  43789  naddgeoa  43837  rp-fakeimass  43954  clublem  44052  grur1cld  44674  ee121  44947  ee122  44948  rspsbc2  44976  ax6e2ndeq  45001  vd12  45042  vd13  45043  ee221  45092  ee212  45094  ee112  45097  ee211  45100  ee210  45102  ee201  45104  ee120  45106  ee021  45108  ee012  45110  ee102  45112  ee03  45182  ee31  45193  ee31an  45195  ee123  45204  ax6e2ndeqVD  45350  ax6e2ndeqALT  45372  refsum2cnlem1  45483  fiiuncl  45511  eliin2f  45549  disjrnmpt2  45633  disjinfi  45637  rnmptbdlem  45699  allbutfi  45837  infxrunb3rnmpt  45871  infrpgernmpt  45908  monoordxrv  45924  mccl  46043  constlimc  46069  limclner  46094  xlimmnfvlem1  46275  xlimpnfvlem1  46279  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnprodlem3  46391  stoweidlem31  46474  pwsal  46758  prsal  46761  sge0pnffigt  46839  sge0ltfirp  46843  0ome  46972  hoicvrrex  46999  hoidmvle  47043  ovnhoilem1  47044  ovnlecvr2  47053  smflimlem3  47216  ormkglobd  47318  chnsubseqword  47321  funressnfv  47488  euoreqb  47554  ndmaovass  47651  afv2orxorb  47673  otiunsndisjX  47724  nltle2tri  47758  nnmul2b  47776  m1modmmod  47809  smonoord  47822  iccpartigtl  47880  icceuelpartlem  47892  iccpartnel  47895  sprsymrelfolem2  47950  prproropf1olem4  47963  paireqne  47968  reupr  47979  reuopreuprim  47983  nprmmul3  47986  fmtnoprmfac1  48025  fmtnoprmfac2  48027  prmdvdsfmtnof1lem2  48045  31prm  48057  lighneallem3  48067  lighneallem4b  48069  lighneallem4  48070  lighneal  48071  nprmdvdsfacm1lem2  48081  ppivalnnnprm  48088  nn0o1gt2ALTV  48167  nn0oALTV  48169  odd2prm2  48191  even3prm2  48192  fpprwppr  48212  stgoldbwt  48249  sbgoldbwt  48250  sbgoldbalt  48254  sbgoldbo  48260  nnsum3primesgbe  48265  wtgoldbnnsum4prm  48275  bgoldbnnsum3prm  48277  bgoldbtbndlem2  48279  bgoldbtbndlem3  48280  bgoldbtbndlem4  48281  bgoldbtbnd  48282  bgoldbachlt  48286  tgblthelfgott  48288  dfclnbgr6  48329  grimco  48362  uhgrimisgrgric  48404  grtriprop  48414  usgrgrtrirex  48423  isubgr3stgrlem6  48444  isubgr3stgrlem8  48446  grlimprclnbgr  48469  grlimgrtri  48476  gpgedg2ov  48539  gpg5nbgrvtx03starlem1  48541  gpg5nbgrvtx03starlem2  48542  gpg5nbgrvtx03starlem3  48543  gpg5nbgrvtx13starlem1  48544  gpg5nbgrvtx13starlem2  48545  gpg5nbgrvtx13starlem3  48546  gpgcubic  48552  gpg5nbgr3star  48554  gpgprismgr4cycllem7  48574  pgnbgreunbgrlem2  48590  gpg5edgnedg  48603  upgrwlkupwlk  48613  rngccatidALTV  48745  ringccatidALTV  48779  lincdifsn  48897  lindslinindimp2lem1  48931  lindsrng01  48941  ldepsnlinc  48981  blen1b  49061  nn0sumshdiglemB  49093  nn0sumshdiglem1  49094  reorelicc  49183  rrx2xpref1o  49191  rrx2plord2  49195  rrxlinesc  49208  line2ylem  49224  line2xlem  49226  thincmon  49905  thincepi  49906