Theorem a1d 26

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 18	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  27  a1i13  28  syl5com  32  mpid  45  syld  48  imim2d  58  syl6ci  72  syl5d  74  syl6d  76  pm2.21d  122  pm2.24d  152  conax1k  172  pm2.521g2  176  pm2.61iii  187  mtod  201  imbi2d  343  adantr  485  jctild  534  jctird  535  anbi2d  641  anbi1d  642  pm3.4  821  impsingle  1650  meredith  1664  stdpc4lem  2100  stdpc4ALT  2102  ax12  2457  ax12vALT  2503  nfsb4t  2533  moexexlem  2656  pm2.61da3ne  3049  ralrimivw  3161  rexlimdvw  3171  reximdv  3180  vtocl2d  3531  reuind  3719  reuan  3852  2reu4  4481  rabeqsnd  4631  tppreqb  4768  ssprsseq  4786  n0snor2el  4793  prnebg  4816  prel12g  4824  elpreqprlem  4826  3elpr2eq  4866  disjord  5093  disjiund  5095  dtruALT2  5331  exneq  5407  propssopi  5481  opthhausdorff  5490  fr0  5629  ssrel2  5761  poltletr  6122  reuop  6283  ordsssuc2  6443  ordnbtwn  6445  ndmfv  6903  fveqres  6915  fmptco  7115  funsndifnop  7138  tpres  7189  fntpb  7197  elunirn  7239  isof1oopb  7313  ndmovord  7590  ordsucelsuc  7806  tfinds  7844  tfindsg  7845  limomss  7855  findsg  7882  finds1  7884  xpexr  7903  resf1extb  7919  bropopvvv  8073  bropfvvvvlem  8074  bropfvvvv  8075  soxp  8113  poseq  8142  suppun  8168  extmptsuppeq  8172  funsssuppss  8174  suppss  8178  suppss2  8184  suppssfv  8186  suppco  8190  mpoxopynvov0  8202  smofvon2  8331  oaordi  8519  oawordeulem  8527  odi  8552  omeulem1  8555  brdomg  8943  snmapen  9023  fopwdom  9061  fodomr  9104  mapxpen  9119  infensuc  9131  fineqvlem  9214  fineqv  9215  fodomfir  9275  finsschain  9304  fsuppun  9335  fsuppunbi  9337  funsnfsupp  9340  dffi3  9379  fisup2g  9417  fisupcl  9418  fiinf2g  9450  infsupprpr  9454  wemapso2  9503  epnsym  9566  en3lplem2  9570  preleqg  9572  inf3lemd  9584  r1ordg  9738  r1val1  9746  r1pw  9805  r1pwALT  9806  rankxplim3  9841  eldju2ndl  9898  eldju2ndr  9899  carddomi2  9944  fidomtri  9967  alephon  10041  alephcard  10042  alephnbtwn  10043  alephordi  10046  iunfictbso  10086  fin23lem30  10314  fin1a2lem10  10381  axdc3lem2  10423  axdc3lem4  10425  alephval2  10545  cfpwsdom  10557  axextnd  10564  axrepnd  10567  axpownd  10574  axregnd  10577  axinfndlem1  10578  fpwwe2lem11  10614  wunfi  10694  addnidpi  10874  pinq  10900  mulgt0sr  11078  dedekind  11361  indval0  12210  nnind  12239  nn1m1nn  12242  nn0n0n1ge2b  12561  nn0lt2  12647  nn0le2is012  12648  uzm1  12884  uzinfi  12940  nn01to3  12953  xrltnsym  13150  xrlttri  13152  xrlttr  13153  qbtwnxr  13214  xltnegi  13230  xnn0xaddcl  13249  xlt2add  13274  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  reltxrnmnf  13357  fzdif1  13621  fzospliti  13708  elfzonlteqm1  13758  fzoopth  13779  elfznelfzo  13790  injresinjlem  13807  injresinj  13808  modfzo0difsn  13967  addmodlteq  13970  ssnn0fi  14009  fsuppmapnn0fiub0  14017  suppssfz  14018  seqfveq2  14048  monoord  14056  seqf1o  14067  seqhomo  14073  expnngt1  14265  faclbnd4lem4  14320  hasheqf1oi  14375  hashrabsn1  14398  hashgt0elex  14425  hash1snb  14444  hashf1lem2  14481  hashf1  14482  seqcoll  14489  hashle2pr  14502  pr2pwpr  14504  hashge2el2difr  14506  swrdnnn0nd  14682  swrdnd0  14683  pfxnd0  14714  swrdswrd  14730  pfxccatin12lem3  14757  pfxccat3  14759  swrdccat3blem  14764  repsdf2  14803  repswsymballbi  14805  cshw0  14819  cshwmodn  14820  cshwn  14822  cshwcl  14823  cshwlen  14824  cshw1  14847  2cshwcshw  14850  cshimadifsn  14854  s3sndisj  14992  s3iunsndisj  14993  relexprelg  15063  relexpnndm  15066  relexpaddg  15078  relexpaddd  15079  rtrclreclem4  15086  relexpindlem  15088  rexuz3  15388  rexanuz2  15389  limsupgre  15520  rlimconst  15583  caurcvg  15716  caucvg  15718  sumss  15763  fsumcl2lem  15770  modfsummods  15833  fsumrlim  15851  fsumo1  15852  fprodcl2lem  15992  dvdsaddre2b  16353  dvdsabseq  16359  mod2eq1n2dvds  16393  nno  16428  sumeven  16433  sumodd  16434  nn0rppwr  16607  nn0seqcvgd  16616  lcmdvds  16654  lcmfunsnlem2  16686  lcmfunsnlem  16687  divgcdcoprm0  16711  ge2nprmge4  16748  exprmfct  16751  rpexp1i  16770  prm23lt5  16862  prm23ge5  16863  pcz  16929  pcadd  16937  pcmptcl  16939  oddprmdvds  16951  prmgaplem6  17104  prmgaplem7  17105  cshwshashlem1  17143  cshwsdisj  17146  prmlem0  17153  setsstruct  17224  ressress  17295  initoeu2lem2  18060  mgm2nsgrplem2  18969  mgm2nsgrplem3  18970  dfgrp2e  19018  dfgrp3e  19094  cyccom  19262  symgextf1  19479  gsmsymgrfix  19486  gsmsymgreq  19490  sylow1lem1  19656  efgsf  19787  efgrelexlema  19807  dprdss  20089  ablfac1eulem  20132  01eq0ringOLD  20603  nrhmzr  20610  funcrngcsetcALT  20714  lssssr  21041  psgnodpm  21695  psrvscafval  22055  mplcoe1  22145  mplcoe5  22148  mpfrcl  22193  mamudm  22509  matmulcell  22559  dmatmul  22611  scmatsgrp1  22636  mavmuldm  22664  mavmulsolcl  22665  mdetunilem9  22734  cramerlem3  22803  cramer0  22804  chpscmatgsumbin  22958  chp0mat  22960  fvmptnn04ifc  22966  fvmptnn04ifd  22967  epttop  23123  neiptopnei  23246  fiuncmp  23518  1stcrest  23567  kgenss  23657  hmeofval  23872  fbun  23954  fgss2  23988  filuni  23999  filssufilg  24025  filufint  24034  hausflimi  24094  hausflim  24095  hauspwpwf1  24101  fclscmp  24144  alexsubALTlem4  24164  ptcmplem3  24168  ptcmplem5  24170  cstucnd  24397  isxmet2d  24441  imasdsf1olem  24487  blfps  24520  blf  24521  metrest  24638  nrginvrcn  24806  nmoge0  24835  nmoleub  24845  fsumcn  24986  cmetcaulem  25404  iscmet3  25409  iscmet2  25410  bcthlem2  25441  ovolicc2lem3  25635  itg2seq  25858  itg2splitlem  25864  itgeq1fOLD  25888  itgeq2  25894  iblcnlem  25905  itgfsum  25943  limcnlp  25994  perfdvf  26019  dvnres  26047  dvmptfsum  26091  c1lip1  26113  dvply2g  26403  taylply2  26485  abelth  26558  cxpsqrtth  26849  rlimcnp  27084  xrlimcnp  27087  jensen  27107  ppiublem1  27320  dchrelbas3  27356  bcmono  27395  zabsle1  27414  gausslemma2dlem0f  27479  gausslemma2dlem1a  27483  gausslemma2dlem4  27487  lgsquad2lem2  27503  2lgslem1a1  27507  2lgslem3  27522  2lgs  27525  2lgsoddprm  27534  2sqlem10  27546  2sqnn  27557  addsqnreup  27561  2sqreultblem  27566  2sqreunnltblem  27569  pntrsumbnd2  27685  pntpbnd1  27704  pntlem3  27727  nolesgn2o  27789  noetalem1  27859  bday0b  27960  leftf  28002  rightf  28003  oldss  28017  addcutslem  28124  negcut  28186  mulcutlem  28278  n0s0suc  28489  n0fincut  28502  n0s0m1  28509  nn1m1nns  28521  axcontlem7  29225  elntg2  29240  ausgrusgrb  29420  usgredg2v  29482  lfuhgr1v0e  29509  subumgredg2  29540  upgrreslem  29559  umgrreslem  29560  fusgrfisbase  29583  nbuhgr  29598  uhgrnbgr0nb  29609  nbgr0edglem  29611  nbgr1vtx  29613  cusgredg  29679  cusgrsizeinds  29707  sizusglecusg  29718  finsumvtxdg2size  29805  ewlkle  29860  upgriswlk  29895  pthdivtx  29981  dfpth2  29983  usgr2trlncl  30014  crctcshwlkn0lem4  30067  wwlksn  30091  iswwlksnon  30107  iswspthsnon  30110  wwlksm1edg  30135  wwlksnfi  30160  2pthdlem1  30184  umgr2wlk  30203  umgrclwwlkge2  30247  clwlkclwwlklem2a  30254  clwlkclwwlk  30258  clwlkclwwlkf1lem2  30261  clwlkclwwlkf  30264  clwwisshclwws  30271  clwwlknlbonbgr1  30295  clwwlknon0  30349  clwwlknonel  30351  clwwlknonex2e  30366  3pthdlem1  30420  eupth2  30495  nfrgr2v  30528  frgr3vlem1  30529  1to2vfriswmgr  30535  1to3vfriswmgr  30536  vdgn1frgrv2  30552  frgrncvvdeqlem9  30563  frgrwopreglem4a  30566  frgrregorufr0  30580  frgrregorufr  30581  2wspmdisj  30593  2clwwlk2clwwlklem  30602  frgrreggt1  30649  frgrreg  30650  frgrregord13  30652  aevdemo  30716  shsvs  31580  0cnop  32236  0cnfn  32237  cnlnssadj  32337  ssmd1  32568  ssmd2  32569  atexch  32638  mdsymlem4  32663  sumdmdlem  32675  ifeqeqx  32794  fmptcof2  32910  padct  32971  nnindf  33072  drng0mxidl  33670  constr01  34044  pwsiga  34432  pwldsys  34459  ldsysgenld  34462  fiunelros  34476  breprexp  34932  bnj151  35177  bnj594  35212  bnj600  35219  trssfir1om  35414  trssfir1omregs  35439  subfacp1lem6  35543  erdszelem8  35556  cvmliftlem7  35649  cvmliftlem10  35652  cvmlift2lem12  35672  sat1el2xp  35737  mrsubfval  35866  msubfval  35882  mclsssvlem  35920  antnestlaw2  36050  funpartfv  36303  endofsegid  36443  broutsideof2  36480  a1i24  36669  nn0prpwlem  36690  nn0prpw  36691  ordcmp  36815  findreccl  36821  axtcond  36846  dfttc2g  36874  dfttc4lem2  36897  bj-cbvaw  37120  bj-cbveaw  37122  bj-ax6e  37147  bj-ax12v3ALT  37168  bj-xpnzex  37451  bj-ideqg1  37663  rdgssun  37879  finxp00  37903  domalom  37905  isinf2  37906  fvineqsneq  37913  wl-spae  38031  wl-nfs1t  38047  poimirlem27  38153  ovoliunnfl  38168  voliunnfl  38170  volsupnfl  38171  itg2addnclem3  38179  itg2addnc  38180  ftc1anc  38207  areacirclem1  38214  sdclem2  38248  fdc  38251  mettrifi  38263  isexid2  38361  zerdivemp1x  38453  smprngopr  38558  mpobi123f  38668  mptbi12f  38672  ac6s6  38678  relcnveq3  38833  mopickr  38877  elrelscnveq3  39133  disjlem14  39407  jca3  39487  ax12fromc15  39536  hbequid  39540  dvelimf-o  39560  ax12eq  39572  ax12el  39573  ax12indalem  39576  ax12inda2ALT  39577  ax12inda2  39578  lfl1dim  39752  lfl1dim2N  39753  lkreqN  39801  cvrexchlem  40050  ps-2  40109  paddasslem14  40464  idldil  40745  isltrn2N  40751  cdleme25a  40984  dibglbN  41797  dihlsscpre  41865  dvh4dimlem  42074  lcfl7N  42132  mapdval2N  42261  dvrelog2b  42690  aks6d1c6lem3  42796  monotoddzzfi  43526  onov0suclim  43858  onmcl  43915  omabs2  43916  tfsconcat0b  43930  naddgeoa  43978  rp-fakeimass  44095  clublem  44193  grur1cld  44815  ee121  45073  ee122  45074  rspsbc2  45102  ax6e2ndeq  45127  vd12  45168  vd13  45169  ee221  45218  ee212  45220  ee112  45223  ee211  45226  ee210  45228  ee201  45230  ee120  45232  ee021  45234  ee012  45236  ee102  45238  ee03  45308  ee31  45319  ee31an  45321  ee123  45330  ax6e2ndeqVD  45476  ax6e2ndeqALT  45498  refsum2cnlem1  45616  fiiuncl  45644  eliin2f  45681  disjrnmpt2  45765  disjinfi  45769  rnmptbdlem  45829  allbutfi  45967  infxrunb3rnmpt  46001  infrpgernmpt  46038  monoordxrv  46054  mccl  46173  constlimc  46199  limclner  46224  xlimmnfvlem1  46405  xlimpnfvlem1  46409  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  dvnprodlem3  46521  stoweidlem31  46604  pwsal  46888  prsal  46891  sge0pnffigt  46969  sge0ltfirp  46973  0ome  47102  hoicvrrex  47129  hoidmvle  47173  ovnhoilem1  47174  ovnlecvr2  47183  smflimlem3  47346  ormkglobd  47450  chnsubseqword  47453  funressnfv  47636  euoreqb  47702  ndmaovass  47799  afv2orxorb  47821  otiunsndisjX  47872  nltle2tri  47906  nnmul2b  47924  m1modmmod  47957  smonoord  47970  iccpartigtl  48028  icceuelpartlem  48040  iccpartnel  48043  sprsymrelfolem2  48098  prproropf1olem4  48111  paireqne  48116  reupr  48127  reuopreuprim  48131  nprmmul3  48134  fmtnoprmfac1  48173  fmtnoprmfac2  48175  prmdvdsfmtnof1lem2  48193  31prm  48205  lighneallem3  48215  lighneallem4b  48217  lighneallem4  48218  lighneal  48219  nprmdvdsfacm1lem2  48229  ppivalnnnprm  48236  nn0o1gt2ALTV  48315  nn0oALTV  48317  odd2prm2  48339  even3prm2  48340  fpprwppr  48360  stgoldbwt  48397  sbgoldbwt  48398  sbgoldbalt  48402  sbgoldbo  48408  nnsum3primesgbe  48413  wtgoldbnnsum4prm  48423  bgoldbnnsum3prm  48425  bgoldbtbndlem2  48427  bgoldbtbndlem3  48428  bgoldbtbndlem4  48429  bgoldbtbnd  48430  bgoldbachlt  48434  tgblthelfgott  48436  dfclnbgr6  48477  grimco  48510  uhgrimisgrgric  48552  grtriprop  48562  usgrgrtrirex  48571  isubgr3stgrlem6  48592  isubgr3stgrlem8  48594  grlimprclnbgr  48617  grlimgrtri  48624  gpgedg2ov  48687  gpg5nbgrvtx03starlem1  48689  gpg5nbgrvtx03starlem2  48690  gpg5nbgrvtx03starlem3  48691  gpg5nbgrvtx13starlem1  48692  gpg5nbgrvtx13starlem2  48693  gpg5nbgrvtx13starlem3  48694  gpgcubic  48700  gpg5nbgr3star  48702  gpgprismgr4cycllem7  48722  pgnbgreunbgrlem2  48738  gpg5edgnedg  48751  upgrwlkupwlk  48761  rngccatidALTV  48893  ringccatidALTV  48927  lincdifsn  49056  lindslinindimp2lem1  49090  lindsrng01  49100  ldepsnlinc  49140  blen1b  49220  nn0sumshdiglemB  49252  nn0sumshdiglem1  49253  reorelicc  49342  rrx2xpref1o  49350  rrx2plord2  49354  rrxlinesc  49367  line2ylem  49383  line2xlem  49385  thincmon  50063  thincepi  50064