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  1759  cbv1v  1761  ralimdaa  2563  reuss2  3443  finds2  4637  ssrel  4751  ssrel2  4753  ssrelrel  4763  funfvima2  5795  tfrlem1  6366  tfrlemi1  6390  tfr1onlemaccex  6406  tfrcllemaccex  6419  tfri3  6425  nneneq  6918  ac6sfi  6959  nnnninfeq  7194  nnnninfeq2  7195  pitonn  7915  nnaddcl  9010  nnmulcl  9011  zaddcllempos  9363  zaddcllemneg  9365  peano5uzti  9434  uzind2  9438  fzind  9441  zindd  9444  uzaddcl  9660  exfzdc  10316  frec2uzltd  10495  frecuzrdgg  10508  seq3val  10552  seqvalcd  10553  seq3clss  10563  monoord  10577  seq3caopr3  10583  seqcaopr3g  10584  seq3f1olemp  10607  seqf1oglem2a  10610  seqf1og  10613  seq3id3  10616  seq3homo  10619  seq3z  10620  seqfeq4g  10623  ser3ge0  10628  exp3vallem  10632  expcllem  10642  expap0  10661  mulexp  10670  expadd  10673  expmul  10676  leexp2r  10685  leexp1a  10686  bernneq  10752  modqexp  10758  nn0ltexp2  10801  apexp1  10810  facdiv  10830  facwordi  10832  faclbnd  10833  faclbnd6  10836  omgadd  10894  seq3coll  10934  cjexp  11058  resqrexlemover  11175  resqrexlemdecn  11177  resqrexlemlo  11178  resqrexlemcalc3  11181  absexp  11244  fsum2d  11600  modfsummod  11623  fsumabs  11630  fsumiun  11642  binom  11649  bcxmas  11654  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  clim2prod  11704  prodfap0  11710  prodfrecap  11711  fprodabs  11781  fprod2d  11788  demoivreALT  11939  dvdsfac  12025  gcdmultiple  12187  rplpwr  12194  nn0seqcvgd  12209  alginv  12215  algcvga  12219  algfx  12220  prmdvdsexp  12316  prmfac1  12320  eulerthlemrprm  12397  eulerthlema  12398  pcmpt  12512  pcfac  12519  prmpwdvds  12524  ennnfoneleminc  12628  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemhom  12632  nninfdclemlt  12668  gsumfzz  13127  mulgnnass  13287  mhmmulg  13293  gsumfzconst  13471  srgmulgass  13545  srgpcomp  13546  lmodvsmmulgdi  13879  cnfldexp  14133  gsumfzfsumlemm  14143  tgcl  14300  dvmptfsum  14961  plycolemc  14994  rpcxpmul2  15149  lgsquad2lem2  15323  nninfsellemdc  15654