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  1745  cbv1v  1747  ralimdaa  2543  reuss2  3417  finds2  4602  ssrel  4716  ssrel2  4718  ssrelrel  4728  funfvima2  5751  tfrlem1  6311  tfrlemi1  6335  tfr1onlemaccex  6351  tfrcllemaccex  6364  tfri3  6370  nneneq  6859  ac6sfi  6900  nnnninfeq  7128  nnnninfeq2  7129  pitonn  7849  nnaddcl  8941  nnmulcl  8942  zaddcllempos  9292  zaddcllemneg  9294  peano5uzti  9363  uzind2  9367  fzind  9370  zindd  9373  uzaddcl  9588  exfzdc  10242  frec2uzltd  10405  frecuzrdgg  10418  seq3val  10460  seqvalcd  10461  seq3clss  10469  monoord  10478  seq3caopr3  10483  seq3f1olemp  10504  seq3id3  10509  seq3homo  10512  seq3z  10513  ser3ge0  10519  exp3vallem  10523  expcllem  10533  expap0  10552  mulexp  10561  expadd  10564  expmul  10567  leexp2r  10576  leexp1a  10577  bernneq  10643  modqexp  10649  nn0ltexp2  10691  apexp1  10700  facdiv  10720  facwordi  10722  faclbnd  10723  faclbnd6  10726  omgadd  10784  seq3coll  10824  cjexp  10904  resqrexlemover  11021  resqrexlemdecn  11023  resqrexlemlo  11024  resqrexlemcalc3  11027  absexp  11090  fsum2d  11445  modfsummod  11468  fsumabs  11475  fsumiun  11487  binom  11494  bcxmas  11499  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  clim2prod  11549  prodfap0  11555  prodfrecap  11556  fprodabs  11626  fprod2d  11633  demoivreALT  11783  dvdsfac  11868  gcdmultiple  12023  rplpwr  12030  nn0seqcvgd  12043  alginv  12049  algcvga  12053  algfx  12054  prmdvdsexp  12150  prmfac1  12154  eulerthlemrprm  12231  eulerthlema  12232  pcmpt  12343  pcfac  12350  prmpwdvds  12355  ennnfoneleminc  12414  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemhom  12418  nninfdclemlt  12454  mulgnnass  13023  mhmmulg  13029  srgmulgass  13177  srgpcomp  13178  lmodvsmmulgdi  13418  cnfldexp  13510  tgcl  13603  nninfsellemdc  14798