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  154  conax1k  174  pm2.521g2  178  pm2.61iii  188  mtod  201  imbi2d  344  adantr  484  jctild  529  jctird  530  anbi2d  631  anbi1d  632  pm3.4  809  impsingle  1629  meredith  1643  stdpc4  2073  ax12  2434  ax12vALT  2481  nfsb4t  2517  nfsb4tALT  2580  moexexlem  2688  pm2.61da3ne  3076  ralrimivw  3150  reximdv  3232  rexlimdvw  3249  vtocl2d  3505  reuind  3692  reuan  3825  rexn0  4412  2reu4  4424  tppreqb  4698  ssprsseq  4718  n0snor2el  4724  prnebg  4746  prel12g  4754  elpreqprlem  4756  3elpr2eq  4799  disjord  5018  disjiund  5020  dtru  5236  propssopi  5363  opthhausdorff  5372  fr0  5498  ssrel2  5623  poltletr  5959  reuop  6112  ordsssuc2  6247  ordnbtwn  6249  ndmfv  6675  fveqres  6687  fmptco  6868  funsndifnop  6890  tpres  6940  fntpb  6949  elunirn  6988  isof1oopb  7057  fvmptopab  7188  ndmovord  7318  ordsucelsuc  7517  tfinds  7554  tfindsg  7555  limomss  7565  findsg  7590  finds1  7592  xpexr  7605  bropopvvv  7768  bropfvvvvlem  7769  bropfvvvv  7770  soxp  7806  suppun  7833  extmptsuppeq  7837  funsssuppss  7839  suppss  7843  suppssov1  7845  suppss2  7847  suppssfv  7849  suppco  7853  mpoxopynvov0  7867  smofvon2  7976  oaordi  8155  oawordeulem  8163  odi  8188  omeulem1  8191  brdomg  8502  snmapen  8573  fopwdom  8608  fodomr  8652  mapxpen  8667  infensuc  8679  onomeneq  8693  fineqvlem  8716  fineqv  8717  xpfi  8773  finsschain  8815  fsuppun  8836  fsuppunbi  8838  funsnfsupp  8841  dffi3  8879  fisup2g  8916  fisupcl  8917  fiinf2g  8948  infsupprpr  8952  wemapso2  9001  epnsym  9056  en3lplem2  9060  preleqg  9062  inf3lemd  9074  r1ordg  9191  r1val1  9199  r1pw  9258  r1pwALT  9259  rankxplim3  9294  eldju2ndl  9337  eldju2ndr  9338  carddomi2  9383  fidomtri  9406  pr2ne  9416  alephon  9480  alephcard  9481  alephnbtwn  9482  alephordi  9485  iunfictbso  9525  fin23lem30  9753  fin1a2lem10  9820  axdc3lem2  9862  axdc3lem4  9864  alephval2  9983  cfpwsdom  9995  axextnd  10002  axrepnd  10005  axpownd  10012  axregnd  10015  axinfndlem1  10016  fpwwe2lem12  10052  wunfi  10132  addnidpi  10312  pinq  10338  mulgt0sr  10516  dedekind  10792  nnind  11643  nn1m1nn  11646  nn0n0n1ge2b  11951  nn0lt2  12033  nn0le2is012  12034  uzm1  12264  uzinfi  12316  nn01to3  12329  xrltnsym  12518  xrlttri  12520  xrlttr  12521  qbtwnxr  12581  xltnegi  12597  xnn0xaddcl  12616  xlt2add  12641  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  reltxrnmnf  12723  fzospliti  13064  elfzonlteqm1  13108  elfznelfzo  13137  injresinjlem  13152  injresinj  13153  modfzo0difsn  13306  addmodlteq  13309  ssnn0fi  13348  fsuppmapnn0fiub0  13356  suppssfz  13357  seqfveq2  13388  monoord  13396  seqf1o  13407  seqhomo  13413  expnngt1  13598  faclbnd4lem4  13652  hasheqf1oi  13708  hashrabsn1  13731  hashgt0elex  13758  hash1snb  13776  hashf1lem2  13810  hashf1  13811  seqcoll  13818  hashle2pr  13831  pr2pwpr  13833  hashge2el2difr  13835  swrdnnn0nd  14009  swrdnd0  14010  pfxnd0  14041  swrdswrd  14058  pfxccatin12lem3  14085  pfxccat3  14087  swrdccat3blem  14092  repsdf2  14131  repswsymballbi  14133  cshw0  14147  cshwmodn  14148  cshwn  14150  cshwcl  14151  cshwlen  14152  cshw1  14175  2cshwcshw  14178  cshimadifsn  14182  s3sndisj  14318  s3iunsndisj  14319  relexprelg  14389  relexpnndm  14392  relexpaddg  14404  relexpaddd  14405  rtrclreclem4  14412  relexpindlem  14414  rexuz3  14700  rexanuz2  14701  limsupgre  14830  rlimconst  14893  caurcvg  15025  caucvg  15027  sumss  15073  fsumcl2lem  15080  modfsummods  15140  fsumrlim  15158  fsumo1  15159  fprodcl2lem  15296  dvdsaddre2b  15649  dvdsabseq  15655  mod2eq1n2dvds  15688  nno  15723  sumeven  15728  sumodd  15729  nn0seqcvgd  15904  lcmdvds  15942  lcmfunsnlem2  15974  lcmfunsnlem  15975  divgcdcoprm0  15999  ge2nprmge4  16035  exprmfct  16038  rpexp1i  16055  prm23lt5  16141  prm23ge5  16142  pcz  16207  pcadd  16215  pcmptcl  16217  oddprmdvds  16229  prmgaplem6  16382  prmgaplem7  16383  cshwshashlem1  16421  cshwsdisj  16424  prmlem0  16431  setsstruct  16515  ressress  16554  initoeu2lem2  17267  mgm2nsgrplem2  18076  mgm2nsgrplem3  18077  dfgrp2e  18121  dfgrp3e  18191  cyccom  18338  symgextf1  18541  gsmsymgrfix  18548  gsmsymgreq  18552  sylow1lem1  18715  efgsf  18847  efgrelexlema  18867  dprdss  19144  ablfac1eulem  19187  lssssr  19718  01eq0ring  20038  psgnodpm  20277  psrvscafval  20628  mplcoe1  20705  mplcoe5  20708  mpfrcl  20757  mamudm  20995  matmulcell  21050  dmatmul  21102  scmatsgrp1  21127  mavmuldm  21155  mavmulsolcl  21156  mdetunilem9  21225  cramerlem3  21294  cramer0  21295  chpscmatgsumbin  21449  chp0mat  21451  fvmptnn04ifc  21457  fvmptnn04ifd  21458  epttop  21614  neiptopnei  21737  fiuncmp  22009  1stcrest  22058  kgenss  22148  hmeofval  22363  fbun  22445  fgss2  22479  filuni  22490  filssufilg  22516  filufint  22525  hausflimi  22585  hausflim  22586  hauspwpwf1  22592  fclscmp  22635  alexsubALTlem4  22655  ptcmplem3  22659  ptcmplem5  22661  cstucnd  22890  isxmet2d  22934  imasdsf1olem  22980  blfps  23013  blf  23014  metrest  23131  nrginvrcn  23298  nmoge0  23327  nmoleub  23337  fsumcn  23475  cmetcaulem  23892  iscmet3  23897  iscmet2  23898  bcthlem2  23929  ovolicc2lem3  24123  itg2seq  24346  itg2splitlem  24352  itgeq1f  24375  itgeq2  24381  iblcnlem  24392  itgfsum  24430  limcnlp  24481  perfdvf  24506  dvnres  24534  dvmptfsum  24578  c1lip1  24600  abelth  25036  cxpsqrtth  25320  rlimcnp  25551  xrlimcnp  25554  jensen  25574  ppiublem1  25786  dchrelbas3  25822  bcmono  25861  zabsle1  25880  gausslemma2dlem0f  25945  gausslemma2dlem1a  25949  gausslemma2dlem4  25953  lgsquad2lem2  25969  2lgslem1a1  25973  2lgslem3  25988  2lgs  25991  2lgsoddprm  26000  2sqlem10  26012  2sqnn  26023  addsqnreup  26027  2sqreultblem  26032  2sqreunnltblem  26035  pntrsumbnd2  26151  pntpbnd1  26170  pntlem3  26193  axcontlem7  26764  elntg2  26779  ausgrusgrb  26958  usgredg2v  27017  lfuhgr1v0e  27044  subumgredg2  27075  upgrreslem  27094  umgrreslem  27095  fusgrfisbase  27118  nbuhgr  27133  uhgrnbgr0nb  27144  nbgr0vtxlem  27145  nbgr1vtx  27148  cusgredg  27214  cusgrsizeinds  27242  sizusglecusg  27253  finsumvtxdg2size  27340  ewlkle  27395  upgriswlk  27430  pthdivtx  27518  usgr2trlncl  27549  crctcshwlkn0lem4  27599  wwlksn  27623  iswwlksnon  27639  iswspthsnon  27642  wwlksm1edg  27667  wwlksnfi  27692  2pthdlem1  27716  umgr2wlk  27735  umgrclwwlkge2  27776  clwlkclwwlklem2a  27783  clwlkclwwlk  27787  clwlkclwwlkf1lem2  27790  clwlkclwwlkf  27793  clwwisshclwws  27800  clwwlknlbonbgr1  27824  clwwlknon0  27878  clwwlknonel  27880  clwwlknonex2e  27895  3pthdlem1  27949  eupth2  28024  nfrgr2v  28057  frgr3vlem1  28058  1to2vfriswmgr  28064  1to3vfriswmgr  28065  vdgn1frgrv2  28081  frgrncvvdeqlem9  28092  frgrwopreglem4a  28095  frgrregorufr0  28109  frgrregorufr  28110  2wspmdisj  28122  2clwwlk2clwwlklem  28131  frgrreggt1  28178  frgrreg  28179  frgrregord13  28181  aevdemo  28245  shsvs  29106  0cnop  29762  0cnfn  29763  cnlnssadj  29863  ssmd1  30094  ssmd2  30095  atexch  30164  mdsymlem4  30189  sumdmdlem  30201  rabeqsnd  30271  ifeqeqx  30309  fmptcof2  30420  padct  30481  nnindf  30561  pwsiga  31499  pwldsys  31526  ldsysgenld  31529  fiunelros  31543  breprexp  32014  bnj151  32259  bnj594  32294  bnj600  32301  subfacp1lem6  32545  erdszelem8  32558  cvmliftlem7  32651  cvmliftlem10  32654  cvmlift2lem12  32674  sat1el2xp  32739  mrsubfval  32868  msubfval  32884  mclsssvlem  32922  trpredlem1  33179  poseq  33208  nolesgn2o  33291  funpartfv  33519  endofsegid  33659  broutsideof2  33696  a1i24  33762  nn0prpwlem  33783  nn0prpw  33784  ordcmp  33908  findreccl  33914  bj-ax6e  34114  bj-ax12v3ALT  34133  bj-dtru  34254  bj-xpnzex  34395  bj-ideqg1  34579  rdgssun  34795  finxp00  34819  domalom  34821  isinf2  34822  fvineqsneq  34829  wl-spae  34926  wl-nfs1t  34942  poimirlem27  35084  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  itg2addnclem3  35110  itg2addnc  35111  ftc1anc  35138  areacirclem1  35145  sdclem2  35180  fdc  35183  mettrifi  35195  isexid2  35293  zerdivemp1x  35385  smprngopr  35490  mpobi123f  35600  mptbi12f  35604  ac6s6  35610  relcnveq3  35738  elrelscnveq3  35891  jca3  36152  ax12fromc15  36201  hbequid  36205  dvelimf-o  36225  ax12eq  36237  ax12el  36238  ax12indalem  36241  ax12inda2ALT  36242  ax12inda2  36243  lfl1dim  36417  lfl1dim2N  36418  lkreqN  36466  cvrexchlem  36715  ps-2  36774  paddasslem14  37129  idldil  37410  isltrn2N  37416  cdleme25a  37649  dibglbN  38462  dihlsscpre  38530  dvh4dimlem  38739  lcfl7N  38797  mapdval2N  38926  sn-dtru  39403  nn0rppwr  39490  monotoddzzfi  39883  rp-fakeimass  40220  clublem  40310  relexpnul  40379  grur1cld  40940  ee121  41211  ee122  41212  rspsbc2  41240  ax6e2ndeq  41265  vd12  41306  vd13  41307  ee221  41356  ee212  41358  ee112  41361  ee211  41364  ee210  41366  ee201  41368  ee120  41370  ee021  41372  ee012  41374  ee102  41376  ee03  41447  ee31  41458  ee31an  41460  ee123  41469  ax6e2ndeqVD  41615  ax6e2ndeqALT  41637  refsum2cnlem1  41666  fiiuncl  41699  eliin2f  41740  disjrnmpt2  41815  disjinfi  41820  rnmptbdlem  41893  allbutfi  42029  infxrunb3rnmpt  42065  infrpgernmpt  42104  monoordxrv  42121  mccl  42240  constlimc  42266  limclner  42293  xlimmnfvlem1  42474  xlimpnfvlem1  42478  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvmptfprod  42587  dvnprodlem3  42590  stoweidlem31  42673  pwsal  42957  prsal  42960  sge0pnffigt  43035  sge0ltfirp  43039  0ome  43168  hoicvrrex  43195  hoidmvle  43239  ovnhoilem1  43240  ovnlecvr2  43249  smflimlem3  43406  funressnfv  43635  euoreqb  43665  ndmaovass  43762  afv2orxorb  43784  otiunsndisjX  43835  nltle2tri  43870  fzoopth  43884  smonoord  43888  iccpartigtl  43940  icceuelpartlem  43952  iccpartnel  43955  sprsymrelfolem2  44010  prproropf1olem4  44023  paireqne  44028  reupr  44039  reuopreuprim  44043  fmtnoprmfac1  44082  fmtnoprmfac2  44084  prmdvdsfmtnof1lem2  44102  31prm  44114  lighneallem3  44125  lighneallem4b  44127  lighneallem4  44128  lighneal  44129  nn0o1gt2ALTV  44212  nn0oALTV  44214  odd2prm2  44236  even3prm2  44237  fpprwppr  44257  stgoldbwt  44294  sbgoldbwt  44295  sbgoldbalt  44299  sbgoldbo  44305  nnsum3primesgbe  44310  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbndlem4  44326  bgoldbtbnd  44327  bgoldbachlt  44331  tgblthelfgott  44333  upgrwlkupwlk  44368  nrhmzr  44497  rngccatidALTV  44613  funcrngcsetcALT  44623  ringccatidALTV  44676  lincdifsn  44833  lindslinindimp2lem1  44867  lindsrng01  44877  ldepsnlinc  44917  m1modmmod  44935  blen1b  45002  nn0sumshdiglemB  45034  nn0sumshdiglem1  45035  reorelicc  45124  rrx2xpref1o  45132  rrx2plord2  45136  rrxlinesc  45149  line2ylem  45165  line2xlem  45167