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 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  41  imim2d  54  imim3i  61  loowoz  102  animpimp2impd  527  cbv1  1686  ralimdaa  2452  reuss2  3295  finds2  4444  ssrel  4555  ssrel2  4557  ssrelrel  4567  funfvima2  5566  tfrlem1  6111  tfrlemi1  6135  tfr1onlemaccex  6151  tfrcllemaccex  6164  tfri3  6170  nneneq  6653  ac6sfi  6694  pitonn  7482  nnaddcl  8540  nnmulcl  8541  zaddcllempos  8885  zaddcllemneg  8887  peano5uzti  8953  uzind2  8957  fzind  8960  zindd  8963  uzaddcl  9173  exfzdc  9800  frec2uzltd  9959  frecuzrdgg  9972  iseqvalt  10019  seq3val  10020  iseqsst  10031  seq3clss  10032  monoord  10042  seq3caopr3  10047  seq3f1olemp  10068  seq3id3  10073  seq3homo  10076  seq3z  10077  ser3ge0  10083  exp3vallem  10087  expcllem  10097  expap0  10116  mulexp  10125  expadd  10128  expmul  10131  leexp2r  10140  leexp1a  10141  bernneq  10205  facdiv  10277  facwordi  10279  faclbnd  10280  faclbnd6  10283  omgadd  10341  seq3coll  10378  cjexp  10458  resqrexlemover  10574  resqrexlemdecn  10576  resqrexlemlo  10577  resqrexlemcalc3  10580  absexp  10643  fsum2d  10994  modfsummod  11017  fsumabs  11024  fsumiun  11036  binom  11043  bcxmas  11048  cvgratnnlemnexp  11083  cvgratnnlemmn  11084  demoivreALT  11228  dvdsfac  11304  gcdmultiple  11452  rplpwr  11459  nn0seqcvgd  11466  alginv  11472  algcvga  11476  algfx  11477  prmdvdsexp  11570  prmfac1  11574  tgcl  11932  nninfalllemn  12619  nninfsellemdc  12623