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  481  jctild  526  jctird  527  anbi2d  629  anbi1d  630  pm3.4  807  impsingle  1630  meredith  1644  stdpc4  2072  ax12  2424  ax12vALT  2470  nfsb4t  2504  moexexlem  2629  pm2.61da3ne  3035  ralrimivw  3105  reximdv  3203  rexlimdvw  3220  vtocl2d  3497  reuind  3689  reuan  3830  rexn0OLD  4446  2reu4  4458  tppreqb  4739  ssprsseq  4759  n0snor2el  4765  prnebg  4787  prel12g  4795  elpreqprlem  4797  3elpr2eq  4839  disjord  5063  disjiund  5065  dtruALT2  5294  dtru  5360  propssopi  5423  opthhausdorff  5432  fr0  5569  ssrel2  5697  poltletr  6042  reuop  6200  ordsssuc2  6358  ordnbtwn  6360  ndmfv  6813  fveqres  6825  fmptco  7010  funsndifnop  7032  tpres  7085  fntpb  7094  elunirn  7133  isof1oopb  7205  fvmptopabOLD  7339  ndmovord  7471  ordsucelsuc  7678  tfinds  7715  tfindsg  7716  limomss  7726  findsg  7755  finds1  7757  xpexr  7774  bropopvvv  7939  bropfvvvvlem  7940  bropfvvvv  7941  soxp  7979  suppun  8009  extmptsuppeq  8013  funsssuppss  8015  suppss  8019  suppssOLD  8020  suppssov1  8023  suppss2  8025  suppssfv  8027  suppco  8031  mpoxopynvov0  8043  smofvon2  8196  oaordi  8386  oawordeulem  8394  odi  8419  omeulem1  8422  brdomg  8755  brdomgOLD  8756  snmapen  8837  fopwdom  8876  fodomr  8924  mapxpen  8939  infensuc  8951  onomeneqOLD  9021  fineqvlem  9046  fineqv  9047  xpfi  9094  finsschain  9135  fsuppun  9156  fsuppunbi  9158  funsnfsupp  9161  dffi3  9199  fisup2g  9236  fisupcl  9237  fiinf2g  9268  infsupprpr  9272  wemapso2  9321  epnsym  9376  en3lplem2  9380  preleqg  9382  inf3lemd  9394  r1ordg  9545  r1val1  9553  r1pw  9612  r1pwALT  9613  rankxplim3  9648  eldju2ndl  9691  eldju2ndr  9692  carddomi2  9737  fidomtri  9760  pr2ne  9770  alephon  9834  alephcard  9835  alephnbtwn  9836  alephordi  9839  iunfictbso  9879  fin23lem30  10107  fin1a2lem10  10174  axdc3lem2  10216  axdc3lem4  10218  alephval2  10337  cfpwsdom  10349  axextnd  10356  axrepnd  10359  axpownd  10366  axregnd  10369  axinfndlem1  10370  fpwwe2lem11  10406  wunfi  10486  addnidpi  10666  pinq  10692  mulgt0sr  10870  dedekind  11147  nnind  12000  nn1m1nn  12003  nn0n0n1ge2b  12310  nn0lt2  12392  nn0le2is012  12393  uzm1  12625  uzinfi  12677  nn01to3  12690  xrltnsym  12880  xrlttri  12882  xrlttr  12883  qbtwnxr  12943  xltnegi  12959  xnn0xaddcl  12978  xlt2add  13003  xrsupsslem  13050  xrinfmsslem  13051  xrub  13055  reltxrnmnf  13085  fzospliti  13428  elfzonlteqm1  13472  elfznelfzo  13501  injresinjlem  13516  injresinj  13517  modfzo0difsn  13672  addmodlteq  13675  ssnn0fi  13714  fsuppmapnn0fiub0  13722  suppssfz  13723  seqfveq2  13754  monoord  13762  seqf1o  13773  seqhomo  13779  expnngt1  13965  faclbnd4lem4  14019  hasheqf1oi  14075  hashrabsn1  14098  hashgt0elex  14125  hash1snb  14143  hashf1lem2  14179  hashf1  14180  seqcoll  14187  hashle2pr  14200  pr2pwpr  14202  hashge2el2difr  14204  swrdnnn0nd  14378  swrdnd0  14379  pfxnd0  14410  swrdswrd  14427  pfxccatin12lem3  14454  pfxccat3  14456  swrdccat3blem  14461  repsdf2  14500  repswsymballbi  14502  cshw0  14516  cshwmodn  14517  cshwn  14519  cshwcl  14520  cshwlen  14521  cshw1  14544  2cshwcshw  14547  cshimadifsn  14551  s3sndisj  14687  s3iunsndisj  14688  relexprelg  14758  relexpnndm  14761  relexpaddg  14773  relexpaddd  14774  rtrclreclem4  14781  relexpindlem  14783  rexuz3  15069  rexanuz2  15070  limsupgre  15199  rlimconst  15262  caurcvg  15397  caucvg  15399  sumss  15445  fsumcl2lem  15452  modfsummods  15514  fsumrlim  15532  fsumo1  15533  fprodcl2lem  15669  dvdsaddre2b  16025  dvdsabseq  16031  mod2eq1n2dvds  16065  nno  16100  sumeven  16105  sumodd  16106  nn0seqcvgd  16284  lcmdvds  16322  lcmfunsnlem2  16354  lcmfunsnlem  16355  divgcdcoprm0  16379  ge2nprmge4  16415  exprmfct  16418  rpexp1i  16437  prm23lt5  16524  prm23ge5  16525  pcz  16591  pcadd  16599  pcmptcl  16601  oddprmdvds  16613  prmgaplem6  16766  prmgaplem7  16767  cshwshashlem1  16806  cshwsdisj  16809  prmlem0  16816  setsstruct  16886  ressress  16967  initoeu2lem2  17739  mgm2nsgrplem2  18567  mgm2nsgrplem3  18568  dfgrp2e  18614  dfgrp3e  18684  cyccom  18831  symgextf1  19038  gsmsymgrfix  19045  gsmsymgreq  19049  sylow1lem1  19212  efgsf  19344  efgrelexlema  19364  dprdss  19641  ablfac1eulem  19684  lssssr  20224  01eq0ring  20552  psgnodpm  20802  psrvscafval  21168  mplcoe1  21247  mplcoe5  21250  mpfrcl  21304  mamudm  21546  matmulcell  21603  dmatmul  21655  scmatsgrp1  21680  mavmuldm  21708  mavmulsolcl  21709  mdetunilem9  21778  cramerlem3  21847  cramer0  21848  chpscmatgsumbin  22002  chp0mat  22004  fvmptnn04ifc  22010  fvmptnn04ifd  22011  epttop  22168  neiptopnei  22292  fiuncmp  22564  1stcrest  22613  kgenss  22703  hmeofval  22918  fbun  23000  fgss2  23034  filuni  23045  filssufilg  23071  filufint  23080  hausflimi  23140  hausflim  23141  hauspwpwf1  23147  fclscmp  23190  alexsubALTlem4  23210  ptcmplem3  23214  ptcmplem5  23216  cstucnd  23445  isxmet2d  23489  imasdsf1olem  23535  blfps  23568  blf  23569  metrest  23689  nrginvrcn  23865  nmoge0  23894  nmoleub  23904  fsumcn  24042  cmetcaulem  24461  iscmet3  24466  iscmet2  24467  bcthlem2  24498  ovolicc2lem3  24692  itg2seq  24916  itg2splitlem  24922  itgeq1f  24945  itgeq2  24951  iblcnlem  24962  itgfsum  25000  limcnlp  25051  perfdvf  25076  dvnres  25104  dvmptfsum  25148  c1lip1  25170  abelth  25609  cxpsqrtth  25893  rlimcnp  26124  xrlimcnp  26127  jensen  26147  ppiublem1  26359  dchrelbas3  26395  bcmono  26434  zabsle1  26453  gausslemma2dlem0f  26518  gausslemma2dlem1a  26522  gausslemma2dlem4  26526  lgsquad2lem2  26542  2lgslem1a1  26546  2lgslem3  26561  2lgs  26564  2lgsoddprm  26573  2sqlem10  26585  2sqnn  26596  addsqnreup  26600  2sqreultblem  26605  2sqreunnltblem  26608  pntrsumbnd2  26724  pntpbnd1  26743  pntlem3  26766  axcontlem7  27347  elntg2  27362  ausgrusgrb  27544  usgredg2v  27603  lfuhgr1v0e  27630  subumgredg2  27661  upgrreslem  27680  umgrreslem  27681  fusgrfisbase  27704  nbuhgr  27719  uhgrnbgr0nb  27730  nbgr0vtxlem  27731  nbgr1vtx  27734  cusgredg  27800  cusgrsizeinds  27828  sizusglecusg  27839  finsumvtxdg2size  27926  ewlkle  27981  upgriswlk  28017  pthdivtx  28106  usgr2trlncl  28137  crctcshwlkn0lem4  28187  wwlksn  28211  iswwlksnon  28227  iswspthsnon  28230  wwlksm1edg  28255  wwlksnfi  28280  2pthdlem1  28304  umgr2wlk  28323  umgrclwwlkge2  28364  clwlkclwwlklem2a  28371  clwlkclwwlk  28375  clwlkclwwlkf1lem2  28378  clwlkclwwlkf  28381  clwwisshclwws  28388  clwwlknlbonbgr1  28412  clwwlknon0  28466  clwwlknonel  28468  clwwlknonex2e  28483  3pthdlem1  28537  eupth2  28612  nfrgr2v  28645  frgr3vlem1  28646  1to2vfriswmgr  28652  1to3vfriswmgr  28653  vdgn1frgrv2  28669  frgrncvvdeqlem9  28680  frgrwopreglem4a  28683  frgrregorufr0  28697  frgrregorufr  28698  2wspmdisj  28710  2clwwlk2clwwlklem  28719  frgrreggt1  28766  frgrreg  28767  frgrregord13  28769  aevdemo  28833  shsvs  29694  0cnop  30350  0cnfn  30351  cnlnssadj  30451  ssmd1  30682  ssmd2  30683  atexch  30752  mdsymlem4  30777  sumdmdlem  30789  rabeqsnd  30857  ifeqeqx  30894  fmptcof2  31003  padct  31063  nnindf  31142  pwsiga  32107  pwldsys  32134  ldsysgenld  32137  fiunelros  32151  breprexp  32622  bnj151  32866  bnj594  32901  bnj600  32908  subfacp1lem6  33156  erdszelem8  33169  cvmliftlem7  33262  cvmliftlem10  33265  cvmlift2lem12  33285  sat1el2xp  33350  mrsubfval  33479  msubfval  33495  mclsssvlem  33533  poxp3  33805  poseq  33811  nolesgn2o  33883  noetalem1  33953  bday0b  34033  leftf  34058  rightf  34059  funpartfv  34256  endofsegid  34396  broutsideof2  34433  a1i24  34499  nn0prpwlem  34520  nn0prpw  34521  ordcmp  34645  findreccl  34651  bj-ax6e  34858  bj-ax12v3ALT  34877  bj-dtru  35008  bj-xpnzex  35158  bj-ideqg1  35344  rdgssun  35558  finxp00  35582  domalom  35584  isinf2  35585  fvineqsneq  35592  wl-spae  35689  wl-nfs1t  35705  poimirlem27  35813  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  itg2addnclem3  35839  itg2addnc  35840  ftc1anc  35867  areacirclem1  35874  sdclem2  35909  fdc  35912  mettrifi  35924  isexid2  36022  zerdivemp1x  36114  smprngopr  36219  mpobi123f  36329  mptbi12f  36333  ac6s6  36339  relcnveq3  36463  elrelscnveq3  36616  jca3  36877  ax12fromc15  36926  hbequid  36930  dvelimf-o  36950  ax12eq  36962  ax12el  36963  ax12indalem  36966  ax12inda2ALT  36967  ax12inda2  36968  lfl1dim  37142  lfl1dim2N  37143  lkreqN  37191  cvrexchlem  37440  ps-2  37499  paddasslem14  37854  idldil  38135  isltrn2N  38141  cdleme25a  38374  dibglbN  39187  dihlsscpre  39255  dvh4dimlem  39464  lcfl7N  39522  mapdval2N  39651  dvrelog2b  40081  sn-dtru  40195  nn0rppwr  40340  monotoddzzfi  40771  rp-fakeimass  41126  clublem  41225  relexpnul  41293  grur1cld  41857  ee121  42132  ee122  42133  rspsbc2  42161  ax6e2ndeq  42186  vd12  42227  vd13  42228  ee221  42277  ee212  42279  ee112  42282  ee211  42285  ee210  42287  ee201  42289  ee120  42291  ee021  42293  ee012  42295  ee102  42297  ee03  42368  ee31  42379  ee31an  42381  ee123  42390  ax6e2ndeqVD  42536  ax6e2ndeqALT  42558  refsum2cnlem1  42587  fiiuncl  42620  eliin2f  42661  disjrnmpt2  42733  disjinfi  42738  rnmptbdlem  42808  allbutfi  42940  infxrunb3rnmpt  42975  infrpgernmpt  43012  monoordxrv  43029  mccl  43146  constlimc  43172  limclner  43199  xlimmnfvlem1  43380  xlimpnfvlem1  43384  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvmptfprod  43493  dvnprodlem3  43496  stoweidlem31  43579  pwsal  43863  prsal  43866  sge0pnffigt  43941  sge0ltfirp  43945  0ome  44074  hoicvrrex  44101  hoidmvle  44145  ovnhoilem1  44146  ovnlecvr2  44155  smflimlem3  44318  funressnfv  44548  euoreqb  44612  ndmaovass  44709  afv2orxorb  44731  otiunsndisjX  44782  nltle2tri  44816  fzoopth  44830  smonoord  44834  iccpartigtl  44886  icceuelpartlem  44898  iccpartnel  44901  sprsymrelfolem2  44956  prproropf1olem4  44969  paireqne  44974  reupr  44985  reuopreuprim  44989  fmtnoprmfac1  45028  fmtnoprmfac2  45030  prmdvdsfmtnof1lem2  45048  31prm  45060  lighneallem3  45070  lighneallem4b  45072  lighneallem4  45073  lighneal  45074  nn0o1gt2ALTV  45157  nn0oALTV  45159  odd2prm2  45181  even3prm2  45182  fpprwppr  45202  stgoldbwt  45239  sbgoldbwt  45240  sbgoldbalt  45244  sbgoldbo  45250  nnsum3primesgbe  45255  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbndlem4  45271  bgoldbtbnd  45272  bgoldbachlt  45276  tgblthelfgott  45278  upgrwlkupwlk  45313  nrhmzr  45442  rngccatidALTV  45558  funcrngcsetcALT  45568  ringccatidALTV  45621  lincdifsn  45776  lindslinindimp2lem1  45810  lindsrng01  45820  ldepsnlinc  45860  m1modmmod  45878  blen1b  45945  nn0sumshdiglemB  45977  nn0sumshdiglem1  45978  reorelicc  46067  rrx2xpref1o  46075  rrx2plord2  46079  rrxlinesc  46092  line2ylem  46108  line2xlem  46110  thincmon  46326  thincepi  46327