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  1791  cbv1v  1793  ralimdaa  2596  reuss2  3484  finds2  4692  ssrel  4806  ssrel2  4808  ssrelrel  4818  funfvima2  5871  tfrlem1  6452  tfrlemi1  6476  tfr1onlemaccex  6492  tfrcllemaccex  6505  tfri3  6511  nneneq  7014  ac6sfi  7056  nnnninfeq  7291  nnnninfeq2  7292  pitonn  8031  nnaddcl  9126  nnmulcl  9127  zaddcllempos  9479  zaddcllemneg  9481  peano5uzti  9551  uzind2  9555  fzind  9558  zindd  9561  uzaddcl  9777  exfzdc  10441  frec2uzltd  10620  frecuzrdgg  10633  seq3val  10677  seqvalcd  10678  seq3clss  10688  monoord  10702  seq3caopr3  10708  seqcaopr3g  10709  seq3f1olemp  10732  seqf1oglem2a  10735  seqf1og  10738  seq3id3  10741  seq3homo  10744  seq3z  10745  seqfeq4g  10748  ser3ge0  10753  exp3vallem  10757  expcllem  10767  expap0  10786  mulexp  10795  expadd  10798  expmul  10801  leexp2r  10810  leexp1a  10811  bernneq  10877  modqexp  10883  nn0ltexp2  10926  apexp1  10935  facdiv  10955  facwordi  10957  faclbnd  10958  faclbnd6  10961  omgadd  11019  seq3coll  11059  cjexp  11399  resqrexlemover  11516  resqrexlemdecn  11518  resqrexlemlo  11519  resqrexlemcalc3  11522  absexp  11585  fsum2d  11941  modfsummod  11964  fsumabs  11971  fsumiun  11983  binom  11990  bcxmas  11995  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  clim2prod  12045  prodfap0  12051  prodfrecap  12052  fprodabs  12122  fprod2d  12129  demoivreALT  12280  dvdsfac  12366  bitsinv1  12468  gcdmultiple  12536  rplpwr  12543  nn0seqcvgd  12558  alginv  12564  algcvga  12568  algfx  12569  prmdvdsexp  12665  prmfac1  12669  eulerthlemrprm  12746  eulerthlema  12747  pcmpt  12861  pcfac  12868  prmpwdvds  12873  ennnfoneleminc  12977  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemhom  12981  nninfdclemlt  13017  gsumfzz  13523  mulgnnass  13689  mhmmulg  13695  gsumfzconst  13873  srgmulgass  13947  srgpcomp  13948  lmodvsmmulgdi  14281  cnfldexp  14535  gsumfzfsumlemm  14545  tgcl  14732  dvmptfsum  15393  plycolemc  15426  rpcxpmul2  15581  lgsquad2lem2  15755  nninfsellemdc  16335  nnnninfex  16347