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  197  imbi2d  341  adantr  482  jctild  527  jctird  528  anbi2d  630  anbi1d  631  pm3.4  809  impsingle  1630  meredith  1644  stdpc4  2072  ax12  2423  ax12vALT  2469  nfsb4t  2499  moexexlem  2623  pm2.61da3ne  3032  ralrimivw  3151  rexlimdvw  3161  reximdv  3171  vtocl2d  3545  reuind  3750  reuan  3891  rexn0OLD  4515  2reu4  4527  rabeqsnd  4672  tppreqb  4809  ssprsseq  4829  n0snor2el  4835  prnebg  4857  prel12g  4865  elpreqprlem  4867  3elpr2eq  4908  disjord  5137  disjiund  5139  dtruALT2  5369  exneq  5436  dtruOLD  5442  propssopi  5509  opthhausdorff  5518  fr0  5656  ssrel2  5786  poltletr  6134  reuop  6293  ordsssuc2  6456  ordnbtwn  6458  ndmfv  6927  fveqres  6939  fmptco  7127  funsndifnop  7149  tpres  7202  fntpb  7211  elunirn  7250  isof1oopb  7322  fvmptopabOLD  7464  ndmovord  7597  ordsucelsuc  7810  tfinds  7849  tfindsg  7850  limomss  7860  findsg  7890  finds1  7892  xpexr  7909  bropopvvv  8076  bropfvvvvlem  8077  bropfvvvv  8078  soxp  8115  poseq  8144  suppun  8169  extmptsuppeq  8173  funsssuppss  8175  suppss  8179  suppssOLD  8180  suppssov1  8183  suppss2  8185  suppssfv  8187  suppco  8191  mpoxopynvov0  8203  smofvon2  8356  oaordi  8546  oawordeulem  8554  odi  8579  omeulem1  8582  brdomg  8952  brdomgOLD  8953  snmapen  9038  fopwdom  9080  fodomr  9128  mapxpen  9143  infensuc  9155  onomeneqOLD  9229  fineqvlem  9262  fineqv  9263  xpfiOLD  9318  finsschain  9359  fsuppun  9382  fsuppunbi  9384  funsnfsupp  9387  dffi3  9426  fisup2g  9463  fisupcl  9464  fiinf2g  9495  infsupprpr  9499  wemapso2  9548  epnsym  9604  en3lplem2  9608  preleqg  9610  inf3lemd  9622  r1ordg  9773  r1val1  9781  r1pw  9840  r1pwALT  9841  rankxplim3  9876  eldju2ndl  9919  eldju2ndr  9920  carddomi2  9965  fidomtri  9988  pr2neOLD  10000  alephon  10064  alephcard  10065  alephnbtwn  10066  alephordi  10069  iunfictbso  10109  fin23lem30  10337  fin1a2lem10  10404  axdc3lem2  10446  axdc3lem4  10448  alephval2  10567  cfpwsdom  10579  axextnd  10586  axrepnd  10589  axpownd  10596  axregnd  10599  axinfndlem1  10600  fpwwe2lem11  10636  wunfi  10716  addnidpi  10896  pinq  10922  mulgt0sr  11100  dedekind  11377  nnind  12230  nn1m1nn  12233  nn0n0n1ge2b  12540  nn0lt2  12625  nn0le2is012  12626  uzm1  12860  uzinfi  12912  nn01to3  12925  xrltnsym  13116  xrlttri  13118  xrlttr  13119  qbtwnxr  13179  xltnegi  13195  xnn0xaddcl  13214  xlt2add  13239  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  reltxrnmnf  13321  fzospliti  13664  elfzonlteqm1  13708  elfznelfzo  13737  injresinjlem  13752  injresinj  13753  modfzo0difsn  13908  addmodlteq  13911  ssnn0fi  13950  fsuppmapnn0fiub0  13958  suppssfz  13959  seqfveq2  13990  monoord  13998  seqf1o  14009  seqhomo  14015  expnngt1  14204  faclbnd4lem4  14256  hasheqf1oi  14311  hashrabsn1  14334  hashgt0elex  14361  hash1snb  14379  hashf1lem2  14417  hashf1  14418  seqcoll  14425  hashle2pr  14438  pr2pwpr  14440  hashge2el2difr  14442  swrdnnn0nd  14606  swrdnd0  14607  pfxnd0  14638  swrdswrd  14655  pfxccatin12lem3  14682  pfxccat3  14684  swrdccat3blem  14689  repsdf2  14728  repswsymballbi  14730  cshw0  14744  cshwmodn  14745  cshwn  14747  cshwcl  14748  cshwlen  14749  cshw1  14772  2cshwcshw  14776  cshimadifsn  14780  s3sndisj  14914  s3iunsndisj  14915  relexprelg  14985  relexpnndm  14988  relexpaddg  15000  relexpaddd  15001  rtrclreclem4  15008  relexpindlem  15010  rexuz3  15295  rexanuz2  15296  limsupgre  15425  rlimconst  15488  caurcvg  15623  caucvg  15625  sumss  15670  fsumcl2lem  15677  modfsummods  15739  fsumrlim  15757  fsumo1  15758  fprodcl2lem  15894  dvdsaddre2b  16250  dvdsabseq  16256  mod2eq1n2dvds  16290  nno  16325  sumeven  16330  sumodd  16331  nn0seqcvgd  16507  lcmdvds  16545  lcmfunsnlem2  16577  lcmfunsnlem  16578  divgcdcoprm0  16602  ge2nprmge4  16638  exprmfct  16641  rpexp1i  16660  prm23lt5  16747  prm23ge5  16748  pcz  16814  pcadd  16822  pcmptcl  16824  oddprmdvds  16836  prmgaplem6  16989  prmgaplem7  16990  cshwshashlem1  17029  cshwsdisj  17032  prmlem0  17039  setsstruct  17109  ressress  17193  initoeu2lem2  17965  mgm2nsgrplem2  18800  mgm2nsgrplem3  18801  dfgrp2e  18848  dfgrp3e  18923  cyccom  19080  symgextf1  19289  gsmsymgrfix  19296  gsmsymgreq  19300  sylow1lem1  19466  efgsf  19597  efgrelexlema  19617  dprdss  19899  ablfac1eulem  19942  01eq0ringOLD  20306  lssssr  20564  psgnodpm  21141  psrvscafval  21509  mplcoe1  21592  mplcoe5  21595  mpfrcl  21648  mamudm  21890  matmulcell  21947  dmatmul  21999  scmatsgrp1  22024  mavmuldm  22052  mavmulsolcl  22053  mdetunilem9  22122  cramerlem3  22191  cramer0  22192  chpscmatgsumbin  22346  chp0mat  22348  fvmptnn04ifc  22354  fvmptnn04ifd  22355  epttop  22512  neiptopnei  22636  fiuncmp  22908  1stcrest  22957  kgenss  23047  hmeofval  23262  fbun  23344  fgss2  23378  filuni  23389  filssufilg  23415  filufint  23424  hausflimi  23484  hausflim  23485  hauspwpwf1  23491  fclscmp  23534  alexsubALTlem4  23554  ptcmplem3  23558  ptcmplem5  23560  cstucnd  23789  isxmet2d  23833  imasdsf1olem  23879  blfps  23912  blf  23913  metrest  24033  nrginvrcn  24209  nmoge0  24238  nmoleub  24248  fsumcn  24386  cmetcaulem  24805  iscmet3  24810  iscmet2  24811  bcthlem2  24842  ovolicc2lem3  25036  itg2seq  25260  itg2splitlem  25266  itgeq1f  25289  itgeq2  25295  iblcnlem  25306  itgfsum  25344  limcnlp  25395  perfdvf  25420  dvnres  25448  dvmptfsum  25492  c1lip1  25514  abelth  25953  cxpsqrtth  26238  rlimcnp  26470  xrlimcnp  26473  jensen  26493  ppiublem1  26705  dchrelbas3  26741  bcmono  26780  zabsle1  26799  gausslemma2dlem0f  26864  gausslemma2dlem1a  26868  gausslemma2dlem4  26872  lgsquad2lem2  26888  2lgslem1a1  26892  2lgslem3  26907  2lgs  26910  2lgsoddprm  26919  2sqlem10  26931  2sqnn  26942  addsqnreup  26946  2sqreultblem  26951  2sqreunnltblem  26954  pntrsumbnd2  27070  pntpbnd1  27089  pntlem3  27112  nolesgn2o  27174  noetalem1  27244  bday0b  27331  leftf  27360  rightf  27361  addscutlem  27461  negscut  27513  mulscutlem  27587  axcontlem7  28228  elntg2  28243  ausgrusgrb  28425  usgredg2v  28484  lfuhgr1v0e  28511  subumgredg2  28542  upgrreslem  28561  umgrreslem  28562  fusgrfisbase  28585  nbuhgr  28600  uhgrnbgr0nb  28611  nbgr0vtxlem  28612  nbgr1vtx  28615  cusgredg  28681  cusgrsizeinds  28709  sizusglecusg  28720  finsumvtxdg2size  28807  ewlkle  28862  upgriswlk  28898  pthdivtx  28986  usgr2trlncl  29017  crctcshwlkn0lem4  29067  wwlksn  29091  iswwlksnon  29107  iswspthsnon  29110  wwlksm1edg  29135  wwlksnfi  29160  2pthdlem1  29184  umgr2wlk  29203  umgrclwwlkge2  29244  clwlkclwwlklem2a  29251  clwlkclwwlk  29255  clwlkclwwlkf1lem2  29258  clwlkclwwlkf  29261  clwwisshclwws  29268  clwwlknlbonbgr1  29292  clwwlknon0  29346  clwwlknonel  29348  clwwlknonex2e  29363  3pthdlem1  29417  eupth2  29492  nfrgr2v  29525  frgr3vlem1  29526  1to2vfriswmgr  29532  1to3vfriswmgr  29533  vdgn1frgrv2  29549  frgrncvvdeqlem9  29560  frgrwopreglem4a  29563  frgrregorufr0  29577  frgrregorufr  29578  2wspmdisj  29590  2clwwlk2clwwlklem  29599  frgrreggt1  29646  frgrreg  29647  frgrregord13  29649  aevdemo  29713  shsvs  30576  0cnop  31232  0cnfn  31233  cnlnssadj  31333  ssmd1  31564  ssmd2  31565  atexch  31634  mdsymlem4  31659  sumdmdlem  31671  ifeqeqx  31774  fmptcof2  31882  padct  31944  nnindf  32025  drng0mxidl  32592  pwsiga  33128  pwldsys  33155  ldsysgenld  33158  fiunelros  33172  breprexp  33645  bnj151  33888  bnj594  33923  bnj600  33930  subfacp1lem6  34176  erdszelem8  34189  cvmliftlem7  34282  cvmliftlem10  34285  cvmlift2lem12  34305  sat1el2xp  34370  mrsubfval  34499  msubfval  34515  mclsssvlem  34553  funpartfv  34917  endofsegid  35057  broutsideof2  35094  a1i24  35186  nn0prpwlem  35207  nn0prpw  35208  ordcmp  35332  findreccl  35338  bj-ax6e  35545  bj-ax12v3ALT  35564  bj-xpnzex  35840  bj-ideqg1  36045  rdgssun  36259  finxp00  36283  domalom  36285  isinf2  36286  fvineqsneq  36293  wl-spae  36390  wl-nfs1t  36406  poimirlem27  36515  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  itg2addnclem3  36541  itg2addnc  36542  ftc1anc  36569  areacirclem1  36576  sdclem2  36610  fdc  36613  mettrifi  36625  isexid2  36723  zerdivemp1x  36815  smprngopr  36920  mpobi123f  37030  mptbi12f  37034  ac6s6  37040  relcnveq3  37190  mopickr  37232  elrelscnveq3  37361  disjlem14  37668  jca3  37726  ax12fromc15  37775  hbequid  37779  dvelimf-o  37799  ax12eq  37811  ax12el  37812  ax12indalem  37815  ax12inda2ALT  37816  ax12inda2  37817  lfl1dim  37991  lfl1dim2N  37992  lkreqN  38040  cvrexchlem  38290  ps-2  38349  paddasslem14  38704  idldil  38985  isltrn2N  38991  cdleme25a  39224  dibglbN  40037  dihlsscpre  40105  dvh4dimlem  40314  lcfl7N  40372  mapdval2N  40501  dvrelog2b  40931  nn0rppwr  41224  monotoddzzfi  41681  onov0suclim  42024  onmcl  42081  omabs2  42082  tfsconcat0b  42096  naddgeoa  42145  rp-fakeimass  42263  clublem  42361  grur1cld  42991  ee121  43266  ee122  43267  rspsbc2  43295  ax6e2ndeq  43320  vd12  43361  vd13  43362  ee221  43411  ee212  43413  ee112  43416  ee211  43419  ee210  43421  ee201  43423  ee120  43425  ee021  43427  ee012  43429  ee102  43431  ee03  43502  ee31  43513  ee31an  43515  ee123  43524  ax6e2ndeqVD  43670  ax6e2ndeqALT  43692  refsum2cnlem1  43721  fiiuncl  43752  eliin2f  43793  disjrnmpt2  43886  disjinfi  43891  rnmptbdlem  43959  allbutfi  44103  infxrunb3rnmpt  44138  infrpgernmpt  44175  monoordxrv  44192  mccl  44314  constlimc  44340  limclner  44367  xlimmnfvlem1  44548  xlimpnfvlem1  44552  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvmptfprod  44661  dvnprodlem3  44664  stoweidlem31  44747  pwsal  45031  prsal  45034  sge0pnffigt  45112  sge0ltfirp  45116  0ome  45245  hoicvrrex  45272  hoidmvle  45316  ovnhoilem1  45317  ovnlecvr2  45326  smflimlem3  45489  funressnfv  45753  euoreqb  45817  ndmaovass  45914  afv2orxorb  45936  otiunsndisjX  45987  nltle2tri  46021  fzoopth  46035  smonoord  46039  iccpartigtl  46091  icceuelpartlem  46103  iccpartnel  46106  sprsymrelfolem2  46161  prproropf1olem4  46174  paireqne  46179  reupr  46190  reuopreuprim  46194  fmtnoprmfac1  46233  fmtnoprmfac2  46235  prmdvdsfmtnof1lem2  46253  31prm  46265  lighneallem3  46275  lighneallem4b  46277  lighneallem4  46278  lighneal  46279  nn0o1gt2ALTV  46362  nn0oALTV  46364  odd2prm2  46386  even3prm2  46387  fpprwppr  46407  stgoldbwt  46444  sbgoldbwt  46445  sbgoldbalt  46449  sbgoldbo  46455  nnsum3primesgbe  46460  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbndlem4  46476  bgoldbtbnd  46477  bgoldbachlt  46481  tgblthelfgott  46483  upgrwlkupwlk  46518  nrhmzr  46647  rngccatidALTV  46887  funcrngcsetcALT  46897  ringccatidALTV  46950  lincdifsn  47105  lindslinindimp2lem1  47139  lindsrng01  47149  ldepsnlinc  47189  m1modmmod  47207  blen1b  47274  nn0sumshdiglemB  47306  nn0sumshdiglem1  47307  reorelicc  47396  rrx2xpref1o  47404  rrx2plord2  47408  rrxlinesc  47421  line2ylem  47437  line2xlem  47439  thincmon  47654  thincepi  47655