Theorem a2d 23

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 6	. 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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  mpdd  36  imim2d  48  imim3i  55  loowoz  96  cbv1  1632  ralimdaa  2386  reuss2  3217  finds2  4324  ssrel  4428  ssrel2  4430  ssrelrel  4440  funfvima2  5391  tfrlem1  5923  tfrlemi1  5946  tfri3  5953  rdgon  5973  nneneq  6320  ac6sfi  6352  pitonn  6924  nnaddcl  7934  nnmulcl  7935  zaddcllempos  8282  zaddcllemneg  8284  peano5uzti  8346  uzind2  8350  fzind  8353  zindd  8356  uzaddcl  8529  frec2uzltd  9189  iseqss  9226  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  iseqcaopr3  9240  iseqid3s  9246  iseqhomo  9248  expivallem  9256  expcllem  9266  expap0  9285  mulexp  9294  expadd  9297  expmul  9300  leexp2r  9308  leexp1a  9309  bernneq  9369  cjexp  9493  resqrexlemover  9608  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc3  9614  absexp  9675  nn0seqcvgd  9880  ialginv  9886  ialgcvga  9890  ialgfx  9891