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  630  anbi1d  631  pm3.4  809  impsingle  1627  meredith  1641  stdpc4  2069  ax12  2421  ax12vALT  2467  nfsb4t  2497  moexexlem  2619  pm2.61da3ne  3014  ralrimivw  3129  rexlimdvw  3139  reximdv  3148  vtocl2d  3528  reuind  3724  reuan  3859  2reu4  4486  rabeqsnd  4633  tppreqb  4769  ssprsseq  4789  n0snor2el  4797  prnebg  4820  prel12g  4828  elpreqprlem  4830  3elpr2eq  4870  disjord  5096  disjiund  5098  dtruALT2  5325  exneq  5395  dtruOLD  5401  propssopi  5468  opthhausdorff  5477  fr0  5616  ssrel2  5748  poltletr  6105  reuop  6266  ordsssuc2  6425  ordnbtwn  6427  ndmfv  6893  fveqres  6905  fmptco  7101  funsndifnop  7123  tpres  7175  fntpb  7183  elunirn  7225  isof1oopb  7300  fvmptopabOLD  7444  ndmovord  7579  ordsucelsuc  7797  tfinds  7836  tfindsg  7837  limomss  7847  findsg  7873  finds1  7875  xpexr  7894  resf1extb  7910  bropopvvv  8069  bropfvvvvlem  8070  bropfvvvv  8071  soxp  8108  poseq  8137  suppun  8163  extmptsuppeq  8167  funsssuppss  8169  suppss  8173  suppss2  8179  suppssfv  8181  suppco  8185  mpoxopynvov0  8197  smofvon2  8325  oaordi  8510  oawordeulem  8518  odi  8543  omeulem1  8546  brdomg  8930  snmapen  9009  fopwdom  9049  fodomr  9092  mapxpen  9107  infensuc  9119  fineqvlem  9209  fineqv  9210  xpfiOLD  9270  fodomfir  9279  finsschain  9310  fsuppun  9338  fsuppunbi  9340  funsnfsupp  9343  dffi3  9382  fisup2g  9420  fisupcl  9421  fiinf2g  9453  infsupprpr  9457  wemapso2  9506  epnsym  9562  en3lplem2  9566  preleqg  9568  inf3lemd  9580  r1ordg  9731  r1val1  9739  r1pw  9798  r1pwALT  9799  rankxplim3  9834  eldju2ndl  9877  eldju2ndr  9878  carddomi2  9923  fidomtri  9946  pr2neOLD  9958  alephon  10022  alephcard  10023  alephnbtwn  10024  alephordi  10027  iunfictbso  10067  fin23lem30  10295  fin1a2lem10  10362  axdc3lem2  10404  axdc3lem4  10406  alephval2  10525  cfpwsdom  10537  axextnd  10544  axrepnd  10547  axpownd  10554  axregnd  10557  axinfndlem1  10558  fpwwe2lem11  10594  wunfi  10674  addnidpi  10854  pinq  10880  mulgt0sr  11058  dedekind  11337  nnind  12204  nn1m1nn  12207  nn0n0n1ge2b  12511  nn0lt2  12597  nn0le2is012  12598  uzm1  12831  uzinfi  12887  nn01to3  12900  xrltnsym  13097  xrlttri  13099  xrlttr  13100  qbtwnxr  13160  xltnegi  13176  xnn0xaddcl  13195  xlt2add  13220  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  reltxrnmnf  13303  fzdif1  13566  fzospliti  13652  elfzonlteqm1  13702  fzoopth  13723  elfznelfzo  13733  injresinjlem  13748  injresinj  13749  modfzo0difsn  13908  addmodlteq  13911  ssnn0fi  13950  fsuppmapnn0fiub0  13958  suppssfz  13959  seqfveq2  13989  monoord  13997  seqf1o  14008  seqhomo  14014  expnngt1  14206  faclbnd4lem4  14261  hasheqf1oi  14316  hashrabsn1  14339  hashgt0elex  14366  hash1snb  14384  hashf1lem2  14421  hashf1  14422  seqcoll  14429  hashle2pr  14442  pr2pwpr  14444  hashge2el2difr  14446  swrdnnn0nd  14621  swrdnd0  14622  pfxnd0  14653  swrdswrd  14670  pfxccatin12lem3  14697  pfxccat3  14699  swrdccat3blem  14704  repsdf2  14743  repswsymballbi  14745  cshw0  14759  cshwmodn  14760  cshwn  14762  cshwcl  14763  cshwlen  14764  cshw1  14787  2cshwcshw  14791  cshimadifsn  14795  s3sndisj  14933  s3iunsndisj  14934  relexprelg  15004  relexpnndm  15007  relexpaddg  15019  relexpaddd  15020  rtrclreclem4  15027  relexpindlem  15029  rexuz3  15315  rexanuz2  15316  limsupgre  15447  rlimconst  15510  caurcvg  15643  caucvg  15645  sumss  15690  fsumcl2lem  15697  modfsummods  15759  fsumrlim  15777  fsumo1  15778  fprodcl2lem  15916  dvdsaddre2b  16277  dvdsabseq  16283  mod2eq1n2dvds  16317  nno  16352  sumeven  16357  sumodd  16358  nn0rppwr  16531  nn0seqcvgd  16540  lcmdvds  16578  lcmfunsnlem2  16610  lcmfunsnlem  16611  divgcdcoprm0  16635  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  17977  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  dfgrp2e  18895  dfgrp3e  18972  cyccom  19135  symgextf1  19351  gsmsymgrfix  19358  gsmsymgreq  19362  sylow1lem1  19528  efgsf  19659  efgrelexlema  19679  dprdss  19961  ablfac1eulem  20004  01eq0ringOLD  20440  nrhmzr  20446  funcrngcsetcALT  20550  lssssr  20860  psgnodpm  21497  psrvscafval  21857  mplcoe1  21944  mplcoe5  21947  mpfrcl  21992  mamudm  22282  matmulcell  22332  dmatmul  22384  scmatsgrp1  22409  mavmuldm  22437  mavmulsolcl  22438  mdetunilem9  22507  cramerlem3  22576  cramer0  22577  chpscmatgsumbin  22731  chp0mat  22733  fvmptnn04ifc  22739  fvmptnn04ifd  22740  epttop  22896  neiptopnei  23019  fiuncmp  23291  1stcrest  23340  kgenss  23430  hmeofval  23645  fbun  23727  fgss2  23761  filuni  23772  filssufilg  23798  filufint  23807  hausflimi  23867  hausflim  23868  hauspwpwf1  23874  fclscmp  23917  alexsubALTlem4  23937  ptcmplem3  23941  ptcmplem5  23943  cstucnd  24171  isxmet2d  24215  imasdsf1olem  24261  blfps  24294  blf  24295  metrest  24412  nrginvrcn  24580  nmoge0  24609  nmoleub  24619  fsumcn  24761  cmetcaulem  25188  iscmet3  25193  iscmet2  25194  bcthlem2  25225  ovolicc2lem3  25420  itg2seq  25643  itg2splitlem  25649  itgeq1fOLD  25673  itgeq2  25679  iblcnlem  25690  itgfsum  25728  limcnlp  25779  perfdvf  25804  dvnres  25833  dvmptfsum  25879  c1lip1  25902  dvply2g  26192  taylply2  26275  abelth  26351  cxpsqrtth  26639  rlimcnp  26875  xrlimcnp  26878  jensen  26899  ppiublem1  27113  dchrelbas3  27149  bcmono  27188  zabsle1  27207  gausslemma2dlem0f  27272  gausslemma2dlem1a  27276  gausslemma2dlem4  27280  lgsquad2lem2  27296  2lgslem1a1  27300  2lgslem3  27315  2lgs  27318  2lgsoddprm  27327  2sqlem10  27339  2sqnn  27350  addsqnreup  27354  2sqreultblem  27359  2sqreunnltblem  27362  pntrsumbnd2  27478  pntpbnd1  27497  pntlem3  27520  nolesgn2o  27583  noetalem1  27653  bday0b  27742  leftf  27777  rightf  27778  addscutlem  27884  negscut  27945  mulscutlem  28034  n0s0suc  28234  n0sfincut  28246  n0s0m1  28252  nn1m1nns  28263  axcontlem7  28897  elntg2  28912  ausgrusgrb  29092  usgredg2v  29154  lfuhgr1v0e  29181  subumgredg2  29212  upgrreslem  29231  umgrreslem  29232  fusgrfisbase  29255  nbuhgr  29270  uhgrnbgr0nb  29281  nbgr0edglem  29283  nbgr1vtx  29285  cusgredg  29351  cusgrsizeinds  29380  sizusglecusg  29391  finsumvtxdg2size  29478  ewlkle  29533  upgriswlk  29569  pthdivtx  29657  dfpth2  29659  usgr2trlncl  29690  crctcshwlkn0lem4  29743  wwlksn  29767  iswwlksnon  29783  iswspthsnon  29786  wwlksm1edg  29811  wwlksnfi  29836  2pthdlem1  29860  umgr2wlk  29879  umgrclwwlkge2  29920  clwlkclwwlklem2a  29927  clwlkclwwlk  29931  clwlkclwwlkf1lem2  29934  clwlkclwwlkf  29937  clwwisshclwws  29944  clwwlknlbonbgr1  29968  clwwlknon0  30022  clwwlknonel  30024  clwwlknonex2e  30039  3pthdlem1  30093  eupth2  30168  nfrgr2v  30201  frgr3vlem1  30202  1to2vfriswmgr  30208  1to3vfriswmgr  30209  vdgn1frgrv2  30225  frgrncvvdeqlem9  30236  frgrwopreglem4a  30239  frgrregorufr0  30253  frgrregorufr  30254  2wspmdisj  30266  2clwwlk2clwwlklem  30275  frgrreggt1  30322  frgrreg  30323  frgrregord13  30325  aevdemo  30389  shsvs  31252  0cnop  31908  0cnfn  31909  cnlnssadj  32009  ssmd1  32240  ssmd2  32241  atexch  32310  mdsymlem4  32335  sumdmdlem  32347  ifeqeqx  32471  fmptcof2  32581  padct  32643  nnindf  32744  drng0mxidl  33447  constr01  33732  pwsiga  34120  pwldsys  34147  ldsysgenld  34150  fiunelros  34164  breprexp  34624  bnj151  34867  bnj594  34902  bnj600  34909  subfacp1lem6  35172  erdszelem8  35185  cvmliftlem7  35278  cvmliftlem10  35281  cvmlift2lem12  35301  sat1el2xp  35366  mrsubfval  35495  msubfval  35511  mclsssvlem  35549  antnestlaw2  35679  funpartfv  35933  endofsegid  36073  broutsideof2  36110  a1i24  36289  nn0prpwlem  36310  nn0prpw  36311  ordcmp  36435  findreccl  36441  bj-ax6e  36656  bj-ax12v3ALT  36674  bj-xpnzex  36947  bj-ideqg1  37152  rdgssun  37366  finxp00  37390  domalom  37392  isinf2  37393  fvineqsneq  37400  wl-spae  37509  wl-nfs1t  37525  poimirlem27  37641  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  itg2addnclem3  37667  itg2addnc  37668  ftc1anc  37695  areacirclem1  37702  sdclem2  37736  fdc  37739  mettrifi  37751  isexid2  37849  zerdivemp1x  37941  smprngopr  38046  mpobi123f  38156  mptbi12f  38160  ac6s6  38166  relcnveq3  38309  mopickr  38345  elrelscnveq3  38482  disjlem14  38790  jca3  38849  ax12fromc15  38898  hbequid  38902  dvelimf-o  38922  ax12eq  38934  ax12el  38935  ax12indalem  38938  ax12inda2ALT  38939  ax12inda2  38940  lfl1dim  39114  lfl1dim2N  39115  lkreqN  39163  cvrexchlem  39413  ps-2  39472  paddasslem14  39827  idldil  40108  isltrn2N  40114  cdleme25a  40347  dibglbN  41160  dihlsscpre  41228  dvh4dimlem  41437  lcfl7N  41495  mapdval2N  41624  dvrelog2b  42054  aks6d1c6lem3  42160  monotoddzzfi  42931  onov0suclim  43263  onmcl  43320  omabs2  43321  tfsconcat0b  43335  naddgeoa  43383  rp-fakeimass  43501  clublem  43599  grur1cld  44221  ee121  44495  ee122  44496  rspsbc2  44524  ax6e2ndeq  44549  vd12  44590  vd13  44591  ee221  44640  ee212  44642  ee112  44645  ee211  44648  ee210  44650  ee201  44652  ee120  44654  ee021  44656  ee012  44658  ee102  44660  ee03  44730  ee31  44741  ee31an  44743  ee123  44752  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  refsum2cnlem1  45031  fiiuncl  45059  eliin2f  45098  disjrnmpt2  45182  disjinfi  45186  rnmptbdlem  45249  allbutfi  45389  infxrunb3rnmpt  45424  infrpgernmpt  45461  monoordxrv  45477  mccl  45596  constlimc  45622  limclner  45649  xlimmnfvlem1  45830  xlimpnfvlem1  45834  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnprodlem3  45946  stoweidlem31  46029  pwsal  46313  prsal  46316  sge0pnffigt  46394  sge0ltfirp  46398  0ome  46527  hoicvrrex  46554  hoidmvle  46598  ovnhoilem1  46599  ovnlecvr2  46608  smflimlem3  46771  ormkglobd  46873  funressnfv  47044  euoreqb  47110  ndmaovass  47207  afv2orxorb  47229  otiunsndisjX  47280  nltle2tri  47314  m1modmmod  47359  smonoord  47372  iccpartigtl  47424  icceuelpartlem  47436  iccpartnel  47439  sprsymrelfolem2  47494  prproropf1olem4  47507  paireqne  47512  reupr  47523  reuopreuprim  47527  fmtnoprmfac1  47566  fmtnoprmfac2  47568  prmdvdsfmtnof1lem2  47586  31prm  47598  lighneallem3  47608  lighneallem4b  47610  lighneallem4  47611  lighneal  47612  nn0o1gt2ALTV  47695  nn0oALTV  47697  odd2prm2  47719  even3prm2  47720  fpprwppr  47740  stgoldbwt  47777  sbgoldbwt  47778  sbgoldbalt  47782  sbgoldbo  47788  nnsum3primesgbe  47793  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  bgoldbachlt  47814  tgblthelfgott  47816  dfclnbgr6  47856  grimco  47889  uhgrimisgrgric  47931  grtriprop  47940  usgrgrtrirex  47949  isubgr3stgrlem6  47970  isubgr3stgrlem8  47972  grlimgrtri  47995  gpgedg2ov  48057  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpgcubic  48070  gpg5nbgr3star  48072  gpgprismgr4cycllem7  48091  pgnbgreunbgrlem2  48107  upgrwlkupwlk  48128  rngccatidALTV  48260  ringccatidALTV  48294  lincdifsn  48413  lindslinindimp2lem1  48447  lindsrng01  48457  ldepsnlinc  48497  blen1b  48577  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  reorelicc  48699  rrx2xpref1o  48707  rrx2plord2  48711  rrxlinesc  48724  line2ylem  48740  line2xlem  48742  thincmon  49422  thincepi  49423