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  119  pm2.24d  149  pm2.51  167  pm2.521  168  pm2.61iii  180  mtod  190  impbid21d  203  imbi2d  332  adantr  474  jctild  521  jctird  522  anbi2d  622  anbi1d  623  pm3.4  800  meredith  1685  ax12  2388  nfsb4t  2464  ax12vALT  2504  moexex  2667  pm2.61da3ne  3058  ralrimivw  3148  reximdv  3196  rexlimdvw  3216  reuind  3627  rexn0  4296  tppreqb  4567  ssprsseq  4587  n0snor2el  4593  prnebg  4617  prel12g  4627  elpreqprlem  4629  3elpr2eq  4670  disjord  4875  disjiund  4877  axsep  5016  dtru  5082  propssopi  5205  opthhausdorff  5214  fr0  5334  ssrel2  5457  poltletr  5783  ordsssuc2  6064  ordnbtwn  6066  ndmfv  6476  fveqres  6489  fmptco  6661  funsndifnop  6682  tpres  6738  fntpb  6745  elunirn  6781  isof1oopb  6847  fvmptopab  6974  ndmovord  7101  ordsucelsuc  7300  tfinds  7337  tfindsg  7338  limomss  7348  findsg  7371  finds1  7373  xpexr  7385  bropopvvv  7536  bropfvvvvlem  7537  bropfvvvv  7538  soxp  7571  suppun  7596  extmptsuppeq  7600  funsssuppss  7603  suppss  7607  suppssov1  7609  suppss2  7611  suppssfv  7613  mpt2xopynvov0  7626  smofvon2  7736  oaordi  7910  oawordeulem  7918  odi  7943  omeulem1  7946  brdomg  8251  snmapen  8322  fopwdom  8356  fodomr  8399  mapxpen  8414  infensuc  8426  onomeneq  8438  fineqvlem  8462  fineqv  8463  xpfi  8519  finsschain  8561  fsuppun  8582  fsuppunbi  8584  funsnfsupp  8587  dffi3  8625  fisup2g  8662  fisupcl  8663  fiinf2g  8694  infsupprpr  8698  wemapso2  8747  epnsym  8801  en3lplem2  8805  preleqg  8807  inf3lemd  8821  r1ordg  8938  r1val1  8946  r1pw  9005  r1pwALT  9006  rankxplim3  9041  eldju2ndl  9083  eldju2ndr  9084  carddomi2  9129  fidomtri  9152  pr2ne  9161  alephon  9225  alephcard  9226  alephnbtwn  9227  alephordi  9230  iunfictbso  9270  fin23lem30  9499  fin1a2lem10  9566  axdc3lem2  9608  axdc3lem4  9610  alephval2  9729  cfpwsdom  9741  axextnd  9748  axrepnd  9751  axpownd  9758  axregnd  9761  axinfndlem1  9762  fpwwe2lem12  9798  wunfi  9878  addnidpi  10058  pinq  10084  mulgt0sr  10262  dedekind  10539  nnind  11394  nn1m1nn  11396  nn0n0n1ge2b  11710  nn0lt2  11792  nn0le2is012  11793  uzm1  12024  uzinfi  12075  nn01to3  12088  xrltnsym  12280  xrlttri  12282  xrlttr  12283  qbtwnxr  12343  xltnegi  12359  xnn0xaddcl  12378  xlt2add  12402  xrsupsslem  12449  xrinfmsslem  12450  xrub  12454  reltxrnmnf  12484  fzospliti  12819  elfzonlteqm1  12863  elfznelfzo  12892  injresinjlem  12907  injresinj  12908  modfzo0difsn  13061  addmodlteq  13064  ssnn0fi  13103  fsuppmapnn0fiub0  13111  suppssfz  13112  seqfveq2  13141  monoord  13149  seqf1o  13160  seqhomo  13166  expnngt1  13347  faclbnd4lem4  13401  hasheqf1oi  13457  hashrabsn1  13478  hashgt0elex  13503  hash1snb  13521  hashf1lem2  13554  hashf1  13555  seqcoll  13562  hashle2pr  13573  pr2pwpr  13575  hashge2el2difr  13577  swrdnnn0nd  13751  swrdnd0  13752  2swrd1eqwrdeqOLD  13774  pfxnd0  13797  swrdswrd  13814  swrdccatin1  13851  swrdccatin12lem3  13860  pfxccat3  13863  swrdccat3OLD  13864  swrdccat3blem  13871  repsdf2  13924  repswsymballbi  13926  cshw0  13945  cshwmodn  13946  cshwn  13948  cshwcl  13949  cshwlen  13950  cshw1  13973  2cshwcshw  13976  cshimadifsn  13980  s3sndisj  14115  s3iunsndisj  14116  relexprelg  14185  relexpnndm  14188  relexpaddg  14200  relexpaddd  14201  rexuz3  14495  rexanuz2  14496  limsupgre  14620  rlimconst  14683  caurcvg  14815  caucvg  14817  sumss  14862  fsumcl2lem  14869  modfsummods  14929  fsumrlim  14947  fsumo1  14948  fprodcl2lem  15083  dvdsaddre2b  15436  dvdsabseq  15442  mod2eq1n2dvds  15475  nno  15512  sumeven  15517  sumodd  15518  nn0seqcvgd  15689  lcmdvds  15727  lcmfunsnlem2  15759  lcmfunsnlem  15760  divgcdcoprm0  15784  exprmfct  15820  rpexp1i  15837  prm23lt5  15923  prm23ge5  15924  pcz  15989  pcadd  15997  pcmptcl  15999  oddprmdvds  16011  prmgaplem6  16164  prmgaplem7  16165  cshwshashlem1  16201  cshwsdisj  16204  prmlem0  16211  setsstruct  16295  ressress  16335  initoeu2lem2  17050  mgm2nsgrplem2  17793  mgm2nsgrplem3  17794  dfgrp2e  17835  dfgrp3e  17902  symgextf1  18224  gsmsymgrfix  18231  gsmsymgreq  18235  sylow1lem1  18397  efgsf  18526  efgrelexlema  18548  dprdss  18815  ablfac1eulem  18858  lssssr  19347  lssssrOLD  19348  01eq0ring  19669  psrvscafval  19787  mplcoe1  19862  mplcoe5  19865  mpfrcl  19914  psgnodpm  20329  mamudm  20598  matmulcell  20655  matmulcellOLD  20656  dmatmul  20708  scmatsgrp1  20733  mavmuldm  20761  mavmulsolcl  20762  mdetunilem9  20831  cramerlem3  20902  cramer0  20903  chpscmatgsumbin  21056  chp0mat  21058  fvmptnn04ifc  21064  fvmptnn04ifd  21065  epttop  21221  neiptopnei  21344  fiuncmp  21616  1stcrest  21665  comppfsc  21744  kgenss  21755  hmeofval  21970  fbun  22052  fgss2  22086  filuni  22097  filssufilg  22123  filufint  22132  hausflimi  22192  hausflim  22193  hauspwpwf1  22199  fclscmp  22242  alexsubALTlem4  22262  ptcmplem3  22266  ptcmplem5  22268  cstucnd  22496  isxmet2d  22540  imasdsf1olem  22586  blfps  22619  blf  22620  metrest  22737  nrginvrcn  22904  nmoge0  22933  nmoleub  22943  fsumcn  23081  cmetcaulem  23494  iscmet3  23499  iscmet2  23500  bcthlem2  23531  ovolicc2lem3  23723  itg2seq  23946  itg2splitlem  23952  itgeq1f  23975  itgeq2  23981  iblcnlem  23992  itgfsum  24030  limcnlp  24079  perfdvf  24104  dvnres  24131  dvmptfsum  24175  c1lip1  24197  abelth  24632  sinq12ge0  24698  cxpsqrtth  24912  rlimcnp  25144  xrlimcnp  25147  jensen  25167  ppiublem1  25379  dchrelbas3  25415  bcmono  25454  zabsle1  25473  gausslemma2dlem0f  25538  gausslemma2dlem1a  25542  gausslemma2dlem4  25546  lgsquad2lem2  25562  2lgslem1a1  25566  2lgslem3  25581  2lgs  25584  2lgsoddprm  25593  2sqlem10  25605  pntrsumbnd2  25708  pntpbnd1  25727  pntlem3  25750  axcontlem7  26319  elntg2  26334  ausgrusgrb  26514  usgredg2v  26573  lfuhgr1v0e  26601  subumgredg2  26632  upgrreslem  26651  umgrreslem  26652  fusgrfisbase  26675  nbuhgr  26690  uhgrnbgr0nb  26701  nbgr0vtxlem  26702  nbgr1vtx  26705  cusgredg  26772  cusgrsizeinds  26800  sizusglecusg  26811  finsumvtxdg2size  26898  ewlkle  26953  upgriswlk  26988  pthdivtx  27081  usgr2trlncl  27112  crctcshwlkn0lem4  27162  wwlksn  27186  iswwlksnon  27202  iswspthsnon  27205  wwlksm1edg  27230  wwlksm1edgOLD  27231  wwlksnfi  27278  wwlksnfiOLD  27279  2pthdlem1  27310  umgr2wlk  27329  umgrclwwlkge2  27371  clwlkclwwlklem2a  27378  clwlkclwwlk  27382  clwlkclwwlkOLD  27383  clwlkclwwlkf1lem2  27387  clwlkclwwlkf1lem2OLD  27388  clwlkclwwlkfOLD  27392  clwlkclwwlkf  27396  clwwisshclwws  27404  clwwlknlbonbgr1  27428  clwwlknfiOLD  27436  wwlksext2clwwlk  27454  clwwlknon0  27495  clwwlknonel  27497  clwwlknonex2e  27512  3pthdlem1  27567  eupth2  27643  nfrgr2v  27680  frgr3vlem1  27681  1to2vfriswmgr  27687  1to3vfriswmgr  27688  vdgn1frgrv2  27704  frgrncvvdeqlem9  27715  frgrwopreglem4a  27718  frgrregorufr0  27732  frgrregorufr  27733  2wspmdisj  27745  2clwwlk2clwwlklem  27757  frgrreggt1  27825  frgrreg  27826  frgrregord13  27828  aevdemo  27892  shsvs  28754  0cnop  29410  0cnfn  29411  cnlnssadj  29511  ssmd1  29742  ssmd2  29743  atexch  29812  mdsymlem4  29837  sumdmdlem  29849  rabeqsnd  29904  ifeqeqx  29924  fmptcof2  30022  padct  30063  nnindf  30129  pwsiga  30791  ldsysgenld  30821  fiunelros  30835  breprexp  31313  bnj151  31546  bnj594  31581  bnj600  31588  subfacp1lem6  31766  erdszelem8  31779  cvmliftlem7  31872  cvmliftlem10  31875  cvmlift2lem12  31895  mrsubfval  32004  msubfval  32020  mclsssvlem  32058  trpredlem1  32315  poseq  32342  nolesgn2o  32413  funpartfv  32641  endofsegid  32781  broutsideof2  32818  a1i24  32884  nn0prpwlem  32905  nn0prpw  32906  ordcmp  33029  findreccl  33035  bj-alsb  33216  bj-ax6e  33243  bj-ax12v3ALT  33265  bj-axsep  33370  bj-dtru  33373  bj-xpnzex  33518  finxp00  33834  cnfinltrel  33836  wl-spae  33902  wl-nfs1t  33918  poimirlem27  34057  ovoliunnfl  34072  voliunnfl  34074  volsupnfl  34075  itg2addnclem3  34083  itg2addnc  34084  ftc1anc  34113  areacirclem1  34120  sdclem2  34157  fdc  34160  mettrifi  34172  isexid2  34273  zerdivemp1x  34365  smprngopr  34470  mpt2bi123f  34588  mptbi12f  34592  ac6s6  34598  relcnveq3  34715  elrelscnveq3  34864  jca3  35005  ax12fromc15  35054  hbequid  35058  dvelimf-o  35078  ax12eq  35090  ax12el  35091  ax12indalem  35094  ax12inda2ALT  35095  ax12inda2  35096  lfl1dim  35270  lfl1dim2N  35271  lkreqN  35319  cvrexchlem  35568  ps-2  35627  paddasslem14  35982  idldil  36263  isltrn2N  36269  cdleme25a  36502  dibglbN  37315  dihlsscpre  37383  dvh4dimlem  37592  lcfl7N  37650  mapdval2N  37779  nn0rppwr  38155  monotoddzzfi  38459  rp-fakeimass  38808  clublem  38867  relexpnul  38920  ee121  39658  ee122  39659  rspsbc2  39687  ax6e2ndeq  39712  vd12  39762  vd13  39763  ee221  39812  ee212  39814  ee112  39817  ee211  39820  ee210  39822  ee201  39824  ee120  39826  ee021  39828  ee012  39830  ee102  39832  ee03  39903  ee31  39914  ee31an  39916  ee123  39925  ax6e2ndeqVD  40071  ax6e2ndeqALT  40093  refsum2cnlem1  40122  fiiuncl  40158  eliin2f  40209  disjrnmpt2  40291  disjinfi  40296  rnmptbd2lem  40367  rnmptbdlem  40374  allbutfi  40515  infxrunb3rnmpt  40554  infrpgernmpt  40593  monoordxrv  40610  mccl  40731  constlimc  40757  limclner  40784  xlimmnfvlem1  40965  xlimpnfvlem1  40969  ioodvbdlimc1lem2  41068  ioodvbdlimc2lem  41070  dvmptfprod  41081  dvnprodlem3  41084  stoweidlem31  41168  pwsal  41452  prsal  41455  sge0pnffigt  41530  sge0ltfirp  41534  0ome  41663  hoicvrrex  41690  hoidmvle  41734  ovnhoilem1  41735  ovnlecvr2  41744  smflimlem3  41901  funressnfv  42100  reuan  42131  euoreqb  42134  2reu4  42144  ndmaovass  42240  afv2orxorb  42262  otiunsndisjX  42313  nltle2tri  42348  fzoopth  42362  smonoord  42366  iccpartigtl  42384  icceuelpartlem  42396  iccpartnel  42399  sprsymrelfolem2  42425  prproropf1olem4  42438  paireqne  42443  fmtnoprmfac1  42491  fmtnoprmfac2  42493  prmdvdsfmtnof1lem2  42511  31prm  42526  lighneallem3  42538  lighneallem4b  42540  lighneallem4  42541  lighneal  42542  nn0o1gt2ALTV  42623  nn0oALTV  42625  odd2prm2  42645  even3prm2  42646  stgoldbwt  42682  sbgoldbwt  42683  sbgoldbalt  42687  sbgoldbo  42693  nnsum3primesgbe  42698  wtgoldbnnsum4prm  42708  bgoldbnnsum3prm  42710  bgoldbtbndlem2  42712  bgoldbtbndlem3  42713  bgoldbtbndlem4  42714  bgoldbtbnd  42715  bgoldbachlt  42719  tgblthelfgott  42721  upgrwlkupwlk  42756  nrhmzr  42881  rngccatidALTV  42997  funcrngcsetcALT  43007  ringccatidALTV  43060  lincdifsn  43221  lindslinindimp2lem1  43255  lindsrng01  43265  ldepsnlinc  43305  m1modmmod  43324  blen1b  43390  nn0sumshdiglemB  43422  nn0sumshdiglem1  43423  reorelicc  43439  rrx2xpref1o  43447  rrx2plord2  43451  rrxlinesc  43464  line2ylem  43480  line2xlem  43482