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  559  cbv1  1791  cbv1v  1793  ralimdaa  2596  reuss2  3484  finds2  4693  ssrel  4807  ssrel2  4809  ssrelrel  4819  funfvima2  5876  tfrlem1  6460  tfrlemi1  6484  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfri3  6519  nneneq  7026  ac6sfi  7068  nnnninfeq  7306  nnnninfeq2  7307  pitonn  8046  nnaddcl  9141  nnmulcl  9142  zaddcllempos  9494  zaddcllemneg  9496  peano5uzti  9566  uzind2  9570  fzind  9573  zindd  9576  uzaddcl  9793  exfzdc  10458  frec2uzltd  10637  frecuzrdgg  10650  seq3val  10694  seqvalcd  10695  seq3clss  10705  monoord  10719  seq3caopr3  10725  seqcaopr3g  10726  seq3f1olemp  10749  seqf1oglem2a  10752  seqf1og  10755  seq3id3  10758  seq3homo  10761  seq3z  10762  seqfeq4g  10765  ser3ge0  10770  exp3vallem  10774  expcllem  10784  expap0  10803  mulexp  10812  expadd  10815  expmul  10818  leexp2r  10827  leexp1a  10828  bernneq  10894  modqexp  10900  nn0ltexp2  10943  apexp1  10952  facdiv  10972  facwordi  10974  faclbnd  10975  faclbnd6  10978  omgadd  11036  seq3coll  11077  cjexp  11419  resqrexlemover  11536  resqrexlemdecn  11538  resqrexlemlo  11539  resqrexlemcalc3  11542  absexp  11605  fsum2d  11961  modfsummod  11984  fsumabs  11991  fsumiun  12003  binom  12010  bcxmas  12015  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  clim2prod  12065  prodfap0  12071  prodfrecap  12072  fprodabs  12142  fprod2d  12149  demoivreALT  12300  dvdsfac  12386  bitsinv1  12488  gcdmultiple  12556  rplpwr  12563  nn0seqcvgd  12578  alginv  12584  algcvga  12588  algfx  12589  prmdvdsexp  12685  prmfac1  12689  eulerthlemrprm  12766  eulerthlema  12767  pcmpt  12881  pcfac  12888  prmpwdvds  12893  ennnfoneleminc  12997  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemhom  13001  nninfdclemlt  13037  gsumfzz  13543  mulgnnass  13709  mhmmulg  13715  gsumfzconst  13893  srgmulgass  13967  srgpcomp  13968  lmodvsmmulgdi  14302  cnfldexp  14556  gsumfzfsumlemm  14566  tgcl  14753  dvmptfsum  15414  plycolemc  15447  rpcxpmul2  15602  lgsquad2lem2  15776  nninfsellemdc  16436  nnnninfex  16448