Theorem a2d 26

Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)

Hypothesis

Ref	Expression
a2d.1	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
a2d	|- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )

Proof of Theorem a2d

Step	Hyp	Ref	Expression
1		a2d.1	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
2		ax-2 7	. 2 |- ( ( ps -> ( ch -> th ) ) -> ( ( ps -> ch ) -> ( ps -> th ) ) )
3	1, 2	syl 14	1 |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  mpdd  41  imim2d  54  imim3i  61  loowoz  103  animpimp2impd  561  cbv1  1794  cbv1v  1796  ralimdaa  2608  reuss2  3501  finds2  4723  ssrel  4838  ssrel2  4840  ssrelrel  4850  funfvima2  5919  tfrlem1  6539  tfrlemi1  6563  tfr1onlemaccex  6579  tfrcllemaccex  6592  tfri3  6598  nneneq  7111  ac6sfi  7155  nnnninfeq  7419  nnnninfeq2  7420  pitonn  8163  nnaddcl  9257  nnmulcl  9258  zaddcllempos  9614  zaddcllemneg  9616  peano5uzti  9686  uzind2  9690  fzind  9693  zindd  9696  uzaddcl  9918  exfzdc  10586  frec2uzltd  10765  frecuzrdgg  10778  seq3val  10822  seqvalcd  10823  seq3clss  10833  monoord  10847  seq3caopr3  10853  seqcaopr3g  10854  seq3f1olemp  10877  seqf1oglem2a  10880  seqf1og  10883  seq3id3  10886  seq3homo  10889  seq3z  10890  seqfeq4g  10893  ser3ge0  10898  exp3vallem  10902  expcllem  10912  expap0  10931  mulexp  10940  expadd  10943  expmul  10946  leexp2r  10955  leexp1a  10956  bernneq  11022  modqexp  11028  nn0ltexp2  11071  apexp1  11080  facdiv  11100  facwordi  11102  faclbnd  11103  faclbnd6  11106  omgadd  11166  hashmap  11192  seq3coll  11214  cjexp  11578  resqrexlemover  11695  resqrexlemdecn  11697  resqrexlemlo  11698  resqrexlemcalc3  11701  absexp  11764  fsum2d  12121  modfsummod  12144  fsumabs  12151  fsumiun  12163  binom  12170  bcxmas  12175  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  clim2prod  12225  prodfap0  12231  prodfrecap  12232  fprodabs  12302  fprod2d  12309  demoivreALT  12460  dvdsfac  12546  bitsinv1  12648  gcdmultiple  12716  rplpwr  12723  nn0seqcvgd  12738  alginv  12744  algcvga  12748  algfx  12749  prmdvdsexp  12845  prmfac1  12849  eulerthlemrprm  12926  eulerthlema  12927  pcmpt  13041  pcfac  13048  prmpwdvds  13053  ennnfoneleminc  13162  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemhom  13166  nninfdclemlt  13202  gsumfzz  13708  mulgnnass  13874  mhmmulg  13880  gsumfzconst  14058  srgmulgass  14133  srgpcomp  14134  lmodvsmmulgdi  14471  cnfldexp  14725  gsumfzfsumlemm  14735  tgcl  14929  dvmptfsum  15590  plycolemc  15623  rpcxpmul2  15778  lgsquad2lem2  15955  eupth2lemsfi  16473  eupth2fi  16474  depindlem2  16502  depindlem3  16503  nninfsellemdc  16788  nnnninfex  16800