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  1657  meredith  1671  stdpc4  2102  ax12  2455  ax12vALT  2501  nfsb4t  2531  moexexlem  2654  pm2.61da3ne  3047  ralrimivw  3161  rexlimdvw  3171  reximdv  3180  vtocl2d  3529  reuind  3717  reuan  3851  2reu4  4486  rabeqsnd  4636  tppreqb  4774  ssprsseq  4792  n0snor2el  4799  prnebg  4822  prel12g  4830  elpreqprlem  4832  3elpr2eq  4872  disjord  5099  disjiund  5101  dtruALT2  5343  exneq  5419  propssopi  5493  opthhausdorff  5502  fr0  5641  ssrel2  5773  poltletr  6134  reuop  6296  ordsssuc2  6456  ordnbtwn  6458  ndmfv  6915  fveqres  6927  fmptco  7127  funsndifnop  7150  tpres  7201  fntpb  7209  elunirn  7251  isof1oopb  7325  ndmovord  7602  ordsucelsuc  7819  tfinds  7857  tfindsg  7858  limomss  7868  findsg  7895  finds1  7897  xpexr  7916  resf1extb  7932  bropopvvv  8086  bropfvvvvlem  8087  bropfvvvv  8088  soxp  8126  poseq  8155  suppun  8181  extmptsuppeq  8185  funsssuppss  8187  suppss  8191  suppss2  8197  suppssfv  8199  suppco  8203  mpoxopynvov0  8215  smofvon2  8344  oaordi  8532  oawordeulem  8540  odi  8565  omeulem1  8568  brdomg  8956  snmapen  9036  fopwdom  9074  fodomr  9117  mapxpen  9132  infensuc  9144  fineqvlem  9227  fineqv  9228  fodomfir  9288  finsschain  9317  fsuppun  9348  fsuppunbi  9350  funsnfsupp  9353  dffi3  9392  fisup2g  9430  fisupcl  9431  fiinf2g  9463  infsupprpr  9467  wemapso2  9516  epnsym  9579  en3lplem2  9583  preleqg  9585  inf3lemd  9597  r1ordg  9751  r1val1  9759  r1pw  9818  r1pwALT  9819  rankxplim3  9854  eldju2ndl  9911  eldju2ndr  9912  carddomi2  9957  fidomtri  9980  alephon  10054  alephcard  10055  alephnbtwn  10056  alephordi  10059  iunfictbso  10099  fin23lem30  10327  fin1a2lem10  10394  axdc3lem2  10436  axdc3lem4  10438  alephval2  10558  cfpwsdom  10570  axextnd  10577  axrepnd  10580  axpownd  10587  axregnd  10590  axinfndlem1  10591  fpwwe2lem11  10627  wunfi  10707  addnidpi  10887  pinq  10913  mulgt0sr  11091  dedekind  11374  indval0  12223  nnind  12252  nn1m1nn  12255  nn0n0n1ge2b  12574  nn0lt2  12660  nn0le2is012  12661  uzm1  12897  uzinfi  12953  nn01to3  12966  xrltnsym  13163  xrlttri  13165  xrlttr  13166  qbtwnxr  13227  xltnegi  13243  xnn0xaddcl  13262  xlt2add  13287  xrsupsslem  13334  xrinfmsslem  13335  xrub  13339  reltxrnmnf  13370  fzdif1  13635  fzospliti  13722  elfzonlteqm1  13772  fzoopth  13793  elfznelfzo  13804  injresinjlem  13821  injresinj  13822  modfzo0difsn  13981  addmodlteq  13984  ssnn0fi  14023  fsuppmapnn0fiub0  14031  suppssfz  14032  seqfveq2  14062  monoord  14070  seqf1o  14081  seqhomo  14087  expnngt1  14279  faclbnd4lem4  14334  hasheqf1oi  14389  hashrabsn1  14412  hashgt0elex  14439  hash1snb  14458  hashf1lem2  14495  hashf1  14496  seqcoll  14503  hashle2pr  14516  pr2pwpr  14518  hashge2el2difr  14520  swrdnnn0nd  14696  swrdnd0  14697  pfxnd0  14728  swrdswrd  14744  pfxccatin12lem3  14771  pfxccat3  14773  swrdccat3blem  14778  repsdf2  14817  repswsymballbi  14819  cshw0  14833  cshwmodn  14834  cshwn  14836  cshwcl  14837  cshwlen  14838  cshw1  14861  2cshwcshw  14864  cshimadifsn  14868  s3sndisj  15006  s3iunsndisj  15007  relexprelg  15077  relexpnndm  15080  relexpaddg  15092  relexpaddd  15093  rtrclreclem4  15100  relexpindlem  15102  rexuz3  15402  rexanuz2  15403  limsupgre  15534  rlimconst  15597  caurcvg  15730  caucvg  15732  sumss  15777  fsumcl2lem  15784  modfsummods  15847  fsumrlim  15865  fsumo1  15866  fprodcl2lem  16006  dvdsaddre2b  16366  dvdsabseq  16372  mod2eq1n2dvds  16406  nno  16441  sumeven  16446  sumodd  16447  nn0rppwr  16620  nn0seqcvgd  16629  lcmdvds  16667  lcmfunsnlem2  16699  lcmfunsnlem  16700  divgcdcoprm0  16724  ge2nprmge4  16761  exprmfct  16764  rpexp1i  16783  prm23lt5  16875  prm23ge5  16876  pcz  16942  pcadd  16950  pcmptcl  16952  oddprmdvds  16964  prmgaplem6  17117  prmgaplem7  17118  cshwshashlem1  17156  cshwsdisj  17159  prmlem0  17166  setsstruct  17237  ressress  17308  initoeu2lem2  18073  mgm2nsgrplem2  18982  mgm2nsgrplem3  18983  dfgrp2e  19031  dfgrp3e  19107  cyccom  19275  symgextf1  19492  gsmsymgrfix  19499  gsmsymgreq  19503  sylow1lem1  19669  efgsf  19800  efgrelexlema  19820  dprdss  20102  ablfac1eulem  20145  01eq0ringOLD  20616  nrhmzr  20623  funcrngcsetcALT  20727  lssssr  21056  isfieldidl  21367  psgnodpm  21719  psrvscafval  22079  mplcoe1  22169  mplcoe5  22172  mpfrcl  22217  mamudm  22533  matmulcell  22583  dmatmul  22635  scmatsgrp1  22660  mavmuldm  22688  mavmulsolcl  22689  mdetunilem9  22758  cramerlem3  22827  cramer0  22828  chpscmatgsumbin  22982  chp0mat  22984  fvmptnn04ifc  22990  fvmptnn04ifd  22991  epttop  23147  neiptopnei  23270  fiuncmp  23542  1stcrest  23591  kgenss  23681  hmeofval  23896  fbun  23978  fgss2  24012  filuni  24023  filssufilg  24049  filufint  24058  hausflimi  24118  hausflim  24119  hauspwpwf1  24125  fclscmp  24168  alexsubALTlem4  24188  ptcmplem3  24192  ptcmplem5  24194  cstucnd  24421  isxmet2d  24465  imasdsf1olem  24511  blfps  24544  blf  24545  metrest  24662  nrginvrcn  24830  nmoge0  24859  nmoleub  24869  fsumcn  25010  cmetcaulem  25428  iscmet3  25433  iscmet2  25434  bcthlem2  25465  ovolicc2lem3  25659  itg2seq  25882  itg2splitlem  25888  itgeq1fOLD  25912  itgeq2  25918  iblcnlem  25929  itgfsum  25967  limcnlp  26018  perfdvf  26043  dvnres  26071  dvmptfsum  26115  c1lip1  26137  dvply2g  26427  taylply2  26512  abelth  26585  cxpsqrtth  26876  rlimcnp  27111  xrlimcnp  27114  jensen  27134  ppiublem1  27347  dchrelbas3  27383  bcmono  27422  zabsle1  27441  gausslemma2dlem0f  27506  gausslemma2dlem1a  27510  gausslemma2dlem4  27514  lgsquad2lem2  27530  2lgslem1a1  27534  2lgslem3  27549  2lgs  27552  2lgsoddprm  27561  2sqlem10  27573  2sqnn  27584  addsqnreup  27588  2sqreultblem  27593  2sqreunnltblem  27596  pntrsumbnd2  27712  pntpbnd1  27731  pntlem3  27754  nolesgn2o  27816  noetalem1  27886  bday0b  27987  leftf  28029  rightf  28030  oldss  28044  addcutslem  28151  negcut  28213  mulcutlem  28305  n0s0suc  28516  n0fincut  28529  n0s0m1  28536  nn1m1nns  28548  axcontlem7  29301  elntg2  29316  ausgrusgrb  29496  usgredg2v  29558  lfuhgr1v0e  29585  subumgredg2  29616  upgrreslem  29635  umgrreslem  29636  fusgrfisbase  29659  nbuhgr  29674  uhgrnbgr0nb  29685  nbgr0edglem  29687  nbgr1vtx  29689  cusgredg  29755  cusgrsizeinds  29783  sizusglecusg  29794  finsumvtxdg2size  29881  ewlkle  29936  upgriswlk  29971  pthdivtx  30057  dfpth2  30059  usgr2trlncl  30090  crctcshwlkn0lem4  30143  wwlksn  30167  iswwlksnon  30183  iswspthsnon  30186  wwlksm1edg  30211  wwlksnfi  30236  2pthdlem1  30260  umgr2wlk  30279  umgrclwwlkge2  30323  clwlkclwwlklem2a  30330  clwlkclwwlk  30334  clwlkclwwlkf1lem2  30337  clwlkclwwlkf  30340  clwwisshclwws  30347  clwwlknlbonbgr1  30371  clwwlknon0  30425  clwwlknonel  30427  clwwlknonex2e  30442  3pthdlem1  30496  eupth2  30571  nfrgr2v  30604  frgr3vlem1  30605  1to2vfriswmgr  30611  1to3vfriswmgr  30612  vdgn1frgrv2  30628  frgrncvvdeqlem9  30639  frgrwopreglem4a  30642  frgrregorufr0  30656  frgrregorufr  30657  2wspmdisj  30669  2clwwlk2clwwlklem  30678  frgrreggt1  30725  frgrreg  30726  frgrregord13  30728  aevdemo  30792  shsvs  31656  0cnop  32312  0cnfn  32313  cnlnssadj  32413  ssmd1  32644  ssmd2  32645  atexch  32714  mdsymlem4  32739  sumdmdlem  32751  ifeqeqx  32869  fmptcof2  32983  padct  33044  nnindf  33145  drng0mxidl  33739  constr01  34113  pwsiga  34501  pwldsys  34528  ldsysgenld  34531  fiunelros  34545  breprexp  35001  bnj151  35246  bnj594  35281  bnj600  35288  trssfir1om  35488  rankscottu  35504  trssfir1omregs  35530  subfacp1lem6  35658  erdszelem8  35671  cvmliftlem7  35764  cvmliftlem10  35767  cvmlift2lem12  35787  sat1el2xp  35852  mrsubfval  35981  msubfval  35997  mclsssvlem  36035  antnestlaw2  36165  funpartfv  36418  endofsegid  36558  broutsideof2  36595  a1i24  36794  nn0prpwlem  36814  nn0prpw  36815  ordcmp  36939  findreccl  36945  axtcond  36970  dfttc2g  36998  dfttc4lem2  37021  bj-cbvaw  37244  bj-cbveaw  37246  bj-ax6e  37271  bj-ax12v3ALT  37292  bj-xpnzex  37576  bj-ideqg1  37789  rdgssun  38005  finxp00  38029  domalom  38031  isinf2  38032  fvineqsneq  38039  wl-spae  38157  wl-nfs1t  38173  poimirlem27  38279  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  itg2addnclem3  38305  itg2addnc  38306  ftc1anc  38333  areacirclem1  38340  sdclem2  38374  fdc  38377  mettrifi  38389  isexid2  38487  zerdivemp1x  38579  smprngopr  38684  mpobi123f  38792  mptbi12f  38796  ac6s6  38802  relcnveq3  38957  mopickr  39001  elrelscnveq3  39257  disjlem14  39531  jca3  39611  ax12fromc15  39660  hbequid  39664  dvelimf-o  39684  ax12eq  39696  ax12el  39697  ax12indalem  39700  ax12inda2ALT  39701  ax12inda2  39702  lfl1dim  39876  lfl1dim2N  39877  lkreqN  39925  cvrexchlem  40174  ps-2  40233  paddasslem14  40588  idldil  40869  isltrn2N  40875  cdleme25a  41108  dibglbN  41921  dihlsscpre  41989  dvh4dimlem  42198  lcfl7N  42256  mapdval2N  42385  dvrelog2b  42814  aks6d1c6lem3  42920  monotoddzzfi  43652  onov0suclim  43984  onmcl  44041  omabs2  44042  tfsconcat0b  44056  naddgeoa  44104  rp-fakeimass  44221  clublem  44319  grur1cld  44939  ee121  45197  ee122  45198  rspsbc2  45226  ax6e2ndeq  45251  vd12  45292  vd13  45293  ee221  45342  ee212  45344  ee112  45347  ee211  45350  ee210  45352  ee201  45354  ee120  45356  ee021  45358  ee012  45360  ee102  45362  ee03  45432  ee31  45443  ee31an  45445  ee123  45454  ax6e2ndeqVD  45600  ax6e2ndeqALT  45622  refsum2cnlem1  45740  fiiuncl  45768  eliin2f  45805  disjrnmpt2  45889  disjinfi  45893  rnmptbdlem  45953  allbutfi  46091  infxrunb3rnmpt  46125  infrpgernmpt  46162  monoordxrv  46178  mccl  46297  constlimc  46323  limclner  46348  xlimmnfvlem1  46529  xlimpnfvlem1  46533  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnprodlem3  46645  stoweidlem31  46728  pwsal  47012  prsal  47015  sge0pnffigt  47093  sge0ltfirp  47097  0ome  47226  hoicvrrex  47253  hoidmvle  47297  ovnhoilem1  47298  ovnlecvr2  47307  smflimlem3  47470  ormkglobd  47574  chnsubseqword  47577  funressnfv  47763  euoreqb  47829  ndmaovass  47926  afv2orxorb  47948  otiunsndisjX  47999  nltle2tri  48033  nnmul2b  48051  m1modmmod  48084  smonoord  48097  iccpartigtl  48155  icceuelpartlem  48167  iccpartnel  48170  sprsymrelfolem2  48225  prproropf1olem4  48238  paireqne  48243  reupr  48254  reuopreuprim  48258  nprmmul3  48261  fmtnoprmfac1  48300  fmtnoprmfac2  48302  prmdvdsfmtnof1lem2  48320  31prm  48332  lighneallem3  48342  lighneallem4b  48344  lighneallem4  48345  lighneal  48346  nprmdvdsfacm1lem2  48356  ppivalnnnprm  48363  nn0o1gt2ALTV  48442  nn0oALTV  48444  odd2prm2  48466  even3prm2  48467  fpprwppr  48487  stgoldbwt  48524  sbgoldbwt  48525  sbgoldbalt  48529  sbgoldbo  48535  nnsum3primesgbe  48540  wtgoldbnnsum4prm  48550  bgoldbnnsum3prm  48552  bgoldbtbndlem2  48554  bgoldbtbndlem3  48555  bgoldbtbndlem4  48556  bgoldbtbnd  48557  bgoldbachlt  48561  tgblthelfgott  48563  dfclnbgr6  48604  grimco  48637  uhgrimisgrgric  48679  grtriprop  48689  usgrgrtrirex  48698  isubgr3stgrlem6  48719  isubgr3stgrlem8  48721  grlimprclnbgr  48744  grlimgrtri  48751  gpgedg2ov  48814  gpg5nbgrvtx03starlem1  48816  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx03starlem3  48818  gpg5nbgrvtx13starlem1  48819  gpg5nbgrvtx13starlem2  48820  gpg5nbgrvtx13starlem3  48821  gpgcubic  48827  gpg5nbgr3star  48829  gpgprismgr4cycllem7  48849  pgnbgreunbgrlem2  48865  gpg5edgnedg  48878  upgrwlkupwlk  48888  rngccatidALTV  49020  ringccatidALTV  49054  lincdifsn  49187  lindslinindimp2lem1  49221  lindsrng01  49231  ldepsnlinc  49271  blen1b  49351  nn0sumshdiglemB  49383  nn0sumshdiglem1  49384  reorelicc  49473  rrx2xpref1o  49481  rrx2plord2  49485  rrxlinesc  49498  line2ylem  49514  line2xlem  49516  thincmon  50194  thincepi  50195