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  200  imbi2d  342  adantr  484  jctild  533  jctird  534  anbi2d  639  anbi1d  640  pm3.4  819  impsingle  1646  meredith  1660  stdpc4lem  2096  stdpc4ALT  2098  ax12  2453  ax12vALT  2499  nfsb4t  2529  moexexlem  2652  pm2.61da3ne  3045  ralrimivw  3157  rexlimdvw  3167  reximdv  3176  vtocl2d  3528  reuind  3715  reuan  3849  2reu4  4477  rabeqsnd  4627  tppreqb  4764  ssprsseq  4782  n0snor2el  4790  prnebg  4813  prel12g  4821  elpreqprlem  4823  3elpr2eq  4863  disjord  5088  disjiund  5090  dtruALT2  5326  exneq  5402  propssopi  5476  opthhausdorff  5485  fr0  5623  ssrel2  5755  poltletr  6116  reuop  6276  ordsssuc2  6435  ordnbtwn  6437  ndmfv  6895  fveqres  6907  fmptco  7107  funsndifnop  7130  tpres  7181  fntpb  7189  elunirn  7231  isof1oopb  7305  ndmovord  7582  ordsucelsuc  7798  tfinds  7836  tfindsg  7837  limomss  7847  findsg  7874  finds1  7876  xpexr  7895  resf1extb  7911  bropopvvv  8064  bropfvvvvlem  8065  bropfvvvv  8066  soxp  8104  poseq  8133  suppun  8159  extmptsuppeq  8163  funsssuppss  8165  suppss  8169  suppss2  8175  suppssfv  8177  suppco  8181  mpoxopynvov0  8193  smofvon2  8322  oaordi  8510  oawordeulem  8518  odi  8543  omeulem1  8546  brdomg  8935  snmapen  9015  fopwdom  9053  fodomr  9096  mapxpen  9111  infensuc  9123  fineqvlem  9206  fineqv  9207  fodomfir  9268  finsschain  9299  fsuppun  9330  fsuppunbi  9332  funsnfsupp  9335  dffi3  9374  fisup2g  9412  fisupcl  9413  fiinf2g  9445  infsupprpr  9449  wemapso2  9498  epnsym  9561  en3lplem2  9565  preleqg  9567  inf3lemd  9579  r1ordg  9733  r1val1  9741  r1pw  9800  r1pwALT  9801  rankxplim3  9836  eldju2ndl  9879  eldju2ndr  9880  carddomi2  9925  fidomtri  9948  alephon  10022  alephcard  10023  alephnbtwn  10024  alephordi  10027  iunfictbso  10067  fin23lem30  10296  fin1a2lem10  10363  axdc3lem2  10405  axdc3lem4  10407  alephval2  10527  cfpwsdom  10539  axextnd  10546  axrepnd  10549  axpownd  10556  axregnd  10559  axinfndlem1  10560  fpwwe2lem11  10596  wunfi  10676  addnidpi  10856  pinq  10882  mulgt0sr  11060  dedekind  11343  indval0  12196  nnind  12225  nn1m1nn  12228  nn0n0n1ge2b  12547  nn0lt2  12633  nn0le2is012  12634  uzm1  12870  uzinfi  12926  nn01to3  12939  xrltnsym  13136  xrlttri  13138  xrlttr  13139  qbtwnxr  13200  xltnegi  13216  xnn0xaddcl  13235  xlt2add  13260  xrsupsslem  13307  xrinfmsslem  13308  xrub  13312  reltxrnmnf  13343  fzdif1  13607  fzospliti  13694  elfzonlteqm1  13744  fzoopth  13765  elfznelfzo  13776  injresinjlem  13793  injresinj  13794  modfzo0difsn  13953  addmodlteq  13956  ssnn0fi  13995  fsuppmapnn0fiub0  14003  suppssfz  14004  seqfveq2  14034  monoord  14042  seqf1o  14053  seqhomo  14059  expnngt1  14251  faclbnd4lem4  14306  hasheqf1oi  14361  hashrabsn1  14384  hashgt0elex  14411  hash1snb  14429  hashf1lem2  14466  hashf1  14467  seqcoll  14474  hashle2pr  14487  pr2pwpr  14489  hashge2el2difr  14491  swrdnnn0nd  14667  swrdnd0  14668  pfxnd0  14699  swrdswrd  14715  pfxccatin12lem3  14742  pfxccat3  14744  swrdccat3blem  14749  repsdf2  14788  repswsymballbi  14790  cshw0  14804  cshwmodn  14805  cshwn  14807  cshwcl  14808  cshwlen  14809  cshw1  14832  2cshwcshw  14835  cshimadifsn  14839  s3sndisj  14977  s3iunsndisj  14978  relexprelg  15048  relexpnndm  15051  relexpaddg  15063  relexpaddd  15064  rtrclreclem4  15071  relexpindlem  15073  rexuz3  15359  rexanuz2  15360  limsupgre  15491  rlimconst  15554  caurcvg  15687  caucvg  15689  sumss  15734  fsumcl2lem  15741  modfsummods  15804  fsumrlim  15822  fsumo1  15823  fprodcl2lem  15963  dvdsaddre2b  16324  dvdsabseq  16330  mod2eq1n2dvds  16364  nno  16399  sumeven  16404  sumodd  16405  nn0rppwr  16578  nn0seqcvgd  16587  lcmdvds  16625  lcmfunsnlem2  16657  lcmfunsnlem  16658  divgcdcoprm0  16682  ge2nprmge4  16719  exprmfct  16722  rpexp1i  16741  prm23lt5  16833  prm23ge5  16834  pcz  16900  pcadd  16908  pcmptcl  16910  oddprmdvds  16922  prmgaplem6  17075  prmgaplem7  17076  cshwshashlem1  17114  cshwsdisj  17117  prmlem0  17124  setsstruct  17195  ressress  17266  initoeu2lem2  18031  mgm2nsgrplem2  18939  mgm2nsgrplem3  18940  dfgrp2e  18988  dfgrp3e  19065  cyccom  19227  symgextf1  19444  gsmsymgrfix  19451  gsmsymgreq  19455  sylow1lem1  19621  efgsf  19752  efgrelexlema  19772  dprdss  20054  ablfac1eulem  20097  01eq0ringOLD  20560  nrhmzr  20566  funcrngcsetcALT  20670  lssssr  21001  psgnodpm  21620  psrvscafval  21980  mplcoe1  22070  mplcoe5  22073  mpfrcl  22118  mamudm  22435  matmulcell  22485  dmatmul  22537  scmatsgrp1  22562  mavmuldm  22590  mavmulsolcl  22591  mdetunilem9  22660  cramerlem3  22729  cramer0  22730  chpscmatgsumbin  22884  chp0mat  22886  fvmptnn04ifc  22892  fvmptnn04ifd  22893  epttop  23049  neiptopnei  23172  fiuncmp  23444  1stcrest  23493  kgenss  23583  hmeofval  23798  fbun  23880  fgss2  23914  filuni  23925  filssufilg  23951  filufint  23960  hausflimi  24020  hausflim  24021  hauspwpwf1  24027  fclscmp  24070  alexsubALTlem4  24090  ptcmplem3  24094  ptcmplem5  24096  cstucnd  24323  isxmet2d  24367  imasdsf1olem  24413  blfps  24446  blf  24447  metrest  24564  nrginvrcn  24732  nmoge0  24761  nmoleub  24771  fsumcn  24912  cmetcaulem  25330  iscmet3  25335  iscmet2  25336  bcthlem2  25367  ovolicc2lem3  25561  itg2seq  25784  itg2splitlem  25790  itgeq1fOLD  25814  itgeq2  25820  iblcnlem  25831  itgfsum  25869  limcnlp  25920  perfdvf  25945  dvnres  25973  dvmptfsum  26017  c1lip1  26039  dvply2g  26326  taylply2  26408  abelth  26481  cxpsqrtth  26772  rlimcnp  27007  xrlimcnp  27010  jensen  27030  ppiublem1  27243  dchrelbas3  27279  bcmono  27318  zabsle1  27337  gausslemma2dlem0f  27402  gausslemma2dlem1a  27406  gausslemma2dlem4  27410  lgsquad2lem2  27426  2lgslem1a1  27430  2lgslem3  27445  2lgs  27448  2lgsoddprm  27457  2sqlem10  27469  2sqnn  27480  addsqnreup  27484  2sqreultblem  27489  2sqreunnltblem  27492  pntrsumbnd2  27608  pntpbnd1  27627  pntlem3  27650  nolesgn2o  27712  noetalem1  27782  bday0b  27883  leftf  27925  rightf  27926  oldss  27940  addcutslem  28047  negcut  28109  mulcutlem  28201  n0s0suc  28412  n0fincut  28425  n0s0m1  28432  nn1m1nns  28444  axcontlem7  29117  elntg2  29132  ausgrusgrb  29312  usgredg2v  29374  lfuhgr1v0e  29401  subumgredg2  29432  upgrreslem  29451  umgrreslem  29452  fusgrfisbase  29475  nbuhgr  29490  uhgrnbgr0nb  29501  nbgr0edglem  29503  nbgr1vtx  29505  cusgredg  29571  cusgrsizeinds  29599  sizusglecusg  29610  finsumvtxdg2size  29697  ewlkle  29752  upgriswlk  29787  pthdivtx  29873  dfpth2  29875  usgr2trlncl  29906  crctcshwlkn0lem4  29959  wwlksn  29983  iswwlksnon  29999  iswspthsnon  30002  wwlksm1edg  30027  wwlksnfi  30052  2pthdlem1  30076  umgr2wlk  30095  umgrclwwlkge2  30139  clwlkclwwlklem2a  30146  clwlkclwwlk  30150  clwlkclwwlkf1lem2  30153  clwlkclwwlkf  30156  clwwisshclwws  30163  clwwlknlbonbgr1  30187  clwwlknon0  30241  clwwlknonel  30243  clwwlknonex2e  30258  3pthdlem1  30312  eupth2  30387  nfrgr2v  30420  frgr3vlem1  30421  1to2vfriswmgr  30427  1to3vfriswmgr  30428  vdgn1frgrv2  30444  frgrncvvdeqlem9  30455  frgrwopreglem4a  30458  frgrregorufr0  30472  frgrregorufr  30473  2wspmdisj  30485  2clwwlk2clwwlklem  30494  frgrreggt1  30541  frgrreg  30542  frgrregord13  30544  aevdemo  30608  shsvs  31472  0cnop  32128  0cnfn  32129  cnlnssadj  32229  ssmd1  32460  ssmd2  32461  atexch  32530  mdsymlem4  32555  sumdmdlem  32567  ifeqeqx  32690  fmptcof2  32809  padct  32870  nnindf  32972  drng0mxidl  33625  constr01  34000  pwsiga  34388  pwldsys  34415  ldsysgenld  34418  fiunelros  34432  breprexp  34891  bnj151  35136  bnj594  35171  bnj600  35178  trssfir1om  35371  trssfir1omregs  35396  subfacp1lem6  35499  erdszelem8  35512  cvmliftlem7  35605  cvmliftlem10  35608  cvmlift2lem12  35628  sat1el2xp  35693  mrsubfval  35822  msubfval  35838  mclsssvlem  35876  antnestlaw2  36006  funpartfv  36259  endofsegid  36399  broutsideof2  36436  a1i24  36625  nn0prpwlem  36646  nn0prpw  36647  ordcmp  36771  findreccl  36777  axtcond  36802  dfttc2g  36830  dfttc4lem2  36853  bj-cbvaw  37077  bj-cbveaw  37079  bj-ax6e  37104  bj-ax12v3ALT  37125  bj-xpnzex  37408  bj-ideqg1  37620  rdgssun  37836  finxp00  37860  domalom  37862  isinf2  37863  fvineqsneq  37870  wl-spae  37988  wl-nfs1t  38004  poimirlem27  38110  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  itg2addnclem3  38136  itg2addnc  38137  ftc1anc  38164  areacirclem1  38171  sdclem2  38205  fdc  38208  mettrifi  38220  isexid2  38318  zerdivemp1x  38410  smprngopr  38515  mpobi123f  38625  mptbi12f  38629  ac6s6  38635  relcnveq3  38790  mopickr  38834  elrelscnveq3  39090  disjlem14  39364  jca3  39444  ax12fromc15  39493  hbequid  39497  dvelimf-o  39517  ax12eq  39529  ax12el  39530  ax12indalem  39533  ax12inda2ALT  39534  ax12inda2  39535  lfl1dim  39709  lfl1dim2N  39710  lkreqN  39758  cvrexchlem  40007  ps-2  40066  paddasslem14  40421  idldil  40702  isltrn2N  40708  cdleme25a  40941  dibglbN  41754  dihlsscpre  41822  dvh4dimlem  42031  lcfl7N  42089  mapdval2N  42218  dvrelog2b  42647  aks6d1c6lem3  42753  monotoddzzfi  43483  onov0suclim  43815  onmcl  43872  omabs2  43873  tfsconcat0b  43887  naddgeoa  43935  rp-fakeimass  44052  clublem  44150  grur1cld  44772  ee121  45045  ee122  45046  rspsbc2  45074  ax6e2ndeq  45099  vd12  45140  vd13  45141  ee221  45190  ee212  45192  ee112  45195  ee211  45198  ee210  45200  ee201  45202  ee120  45204  ee021  45206  ee012  45208  ee102  45210  ee03  45280  ee31  45291  ee31an  45293  ee123  45302  ax6e2ndeqVD  45448  ax6e2ndeqALT  45470  refsum2cnlem1  45581  fiiuncl  45609  eliin2f  45646  disjrnmpt2  45730  disjinfi  45734  rnmptbdlem  45794  allbutfi  45932  infxrunb3rnmpt  45966  infrpgernmpt  46003  monoordxrv  46019  mccl  46138  constlimc  46164  limclner  46189  xlimmnfvlem1  46370  xlimpnfvlem1  46374  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvnprodlem3  46486  stoweidlem31  46569  pwsal  46853  prsal  46856  sge0pnffigt  46934  sge0ltfirp  46938  0ome  47067  hoicvrrex  47094  hoidmvle  47138  ovnhoilem1  47139  ovnlecvr2  47148  smflimlem3  47311  ormkglobd  47415  chnsubseqword  47418  funressnfv  47601  euoreqb  47667  ndmaovass  47764  afv2orxorb  47786  otiunsndisjX  47837  nltle2tri  47871  nnmul2b  47889  m1modmmod  47922  smonoord  47935  iccpartigtl  47993  icceuelpartlem  48005  iccpartnel  48008  sprsymrelfolem2  48063  prproropf1olem4  48076  paireqne  48081  reupr  48092  reuopreuprim  48096  nprmmul3  48099  fmtnoprmfac1  48138  fmtnoprmfac2  48140  prmdvdsfmtnof1lem2  48158  31prm  48170  lighneallem3  48180  lighneallem4b  48182  lighneallem4  48183  lighneal  48184  nprmdvdsfacm1lem2  48194  ppivalnnnprm  48201  nn0o1gt2ALTV  48280  nn0oALTV  48282  odd2prm2  48304  even3prm2  48305  fpprwppr  48325  stgoldbwt  48362  sbgoldbwt  48363  sbgoldbalt  48367  sbgoldbo  48373  nnsum3primesgbe  48378  wtgoldbnnsum4prm  48388  bgoldbnnsum3prm  48390  bgoldbtbndlem2  48392  bgoldbtbndlem3  48393  bgoldbtbndlem4  48394  bgoldbtbnd  48395  bgoldbachlt  48399  tgblthelfgott  48401  dfclnbgr6  48442  grimco  48475  uhgrimisgrgric  48517  grtriprop  48527  usgrgrtrirex  48536  isubgr3stgrlem6  48557  isubgr3stgrlem8  48559  grlimprclnbgr  48582  grlimgrtri  48589  gpgedg2ov  48652  gpg5nbgrvtx03starlem1  48654  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx03starlem3  48656  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem2  48658  gpg5nbgrvtx13starlem3  48659  gpgcubic  48665  gpg5nbgr3star  48667  gpgprismgr4cycllem7  48687  pgnbgreunbgrlem2  48703  gpg5edgnedg  48716  upgrwlkupwlk  48726  rngccatidALTV  48858  ringccatidALTV  48892  lincdifsn  49010  lindslinindimp2lem1  49044  lindsrng01  49054  ldepsnlinc  49094  blen1b  49174  nn0sumshdiglemB  49206  nn0sumshdiglem1  49207  reorelicc  49296  rrx2xpref1o  49304  rrx2plord2  49308  rrxlinesc  49321  line2ylem  49337  line2xlem  49339  thincmon  50018  thincepi  50019