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  1756  cbv1v  1758  ralimdaa  2556  reuss2  3430  finds2  4618  ssrel  4732  ssrel2  4734  ssrelrel  4744  funfvima2  5769  tfrlem1  6332  tfrlemi1  6356  tfr1onlemaccex  6372  tfrcllemaccex  6385  tfri3  6391  nneneq  6884  ac6sfi  6925  nnnninfeq  7155  nnnninfeq2  7156  pitonn  7876  nnaddcl  8968  nnmulcl  8969  zaddcllempos  9319  zaddcllemneg  9321  peano5uzti  9390  uzind2  9394  fzind  9397  zindd  9400  uzaddcl  9615  exfzdc  10269  frec2uzltd  10433  frecuzrdgg  10446  seq3val  10488  seqvalcd  10489  seq3clss  10497  monoord  10506  seq3caopr3  10511  seq3f1olemp  10532  seq3id3  10537  seq3homo  10540  seq3z  10541  ser3ge0  10547  exp3vallem  10551  expcllem  10561  expap0  10580  mulexp  10589  expadd  10592  expmul  10595  leexp2r  10604  leexp1a  10605  bernneq  10671  modqexp  10677  nn0ltexp2  10720  apexp1  10729  facdiv  10749  facwordi  10751  faclbnd  10752  faclbnd6  10755  omgadd  10813  seq3coll  10853  cjexp  10933  resqrexlemover  11050  resqrexlemdecn  11052  resqrexlemlo  11053  resqrexlemcalc3  11056  absexp  11119  fsum2d  11474  modfsummod  11497  fsumabs  11504  fsumiun  11516  binom  11523  bcxmas  11528  cvgratnnlemnexp  11563  cvgratnnlemmn  11564  clim2prod  11578  prodfap0  11584  prodfrecap  11585  fprodabs  11655  fprod2d  11662  demoivreALT  11812  dvdsfac  11897  gcdmultiple  12052  rplpwr  12059  nn0seqcvgd  12072  alginv  12078  algcvga  12082  algfx  12083  prmdvdsexp  12179  prmfac1  12183  eulerthlemrprm  12260  eulerthlema  12261  pcmpt  12374  pcfac  12381  prmpwdvds  12386  ennnfoneleminc  12461  ennnfonelemkh  12462  ennnfonelemhf1o  12463  ennnfonelemhom  12465  nninfdclemlt  12501  mulgnnass  13094  mhmmulg  13100  srgmulgass  13340  srgpcomp  13341  lmodvsmmulgdi  13636  cnfldexp  13877  tgcl  14016  nninfsellemdc  15213