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  3485  finds2  4697  ssrel  4812  ssrel2  4814  ssrelrel  4824  funfvima2  5882  tfrlem1  6469  tfrlemi1  6493  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfri3  6528  nneneq  7038  ac6sfi  7080  nnnninfeq  7318  nnnninfeq2  7319  pitonn  8058  nnaddcl  9153  nnmulcl  9154  zaddcllempos  9506  zaddcllemneg  9508  peano5uzti  9578  uzind2  9582  fzind  9585  zindd  9588  uzaddcl  9810  exfzdc  10476  frec2uzltd  10655  frecuzrdgg  10668  seq3val  10712  seqvalcd  10713  seq3clss  10723  monoord  10737  seq3caopr3  10743  seqcaopr3g  10744  seq3f1olemp  10767  seqf1oglem2a  10770  seqf1og  10773  seq3id3  10776  seq3homo  10779  seq3z  10780  seqfeq4g  10783  ser3ge0  10788  exp3vallem  10792  expcllem  10802  expap0  10821  mulexp  10830  expadd  10833  expmul  10836  leexp2r  10845  leexp1a  10846  bernneq  10912  modqexp  10918  nn0ltexp2  10961  apexp1  10970  facdiv  10990  facwordi  10992  faclbnd  10993  faclbnd6  10996  omgadd  11055  seq3coll  11096  cjexp  11444  resqrexlemover  11561  resqrexlemdecn  11563  resqrexlemlo  11564  resqrexlemcalc3  11567  absexp  11630  fsum2d  11986  modfsummod  12009  fsumabs  12016  fsumiun  12028  binom  12035  bcxmas  12040  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  clim2prod  12090  prodfap0  12096  prodfrecap  12097  fprodabs  12167  fprod2d  12174  demoivreALT  12325  dvdsfac  12411  bitsinv1  12513  gcdmultiple  12581  rplpwr  12588  nn0seqcvgd  12603  alginv  12609  algcvga  12613  algfx  12614  prmdvdsexp  12710  prmfac1  12714  eulerthlemrprm  12791  eulerthlema  12792  pcmpt  12906  pcfac  12913  prmpwdvds  12918  ennnfoneleminc  13022  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemhom  13026  nninfdclemlt  13062  gsumfzz  13568  mulgnnass  13734  mhmmulg  13740  gsumfzconst  13918  srgmulgass  13992  srgpcomp  13993  lmodvsmmulgdi  14327  cnfldexp  14581  gsumfzfsumlemm  14591  tgcl  14778  dvmptfsum  15439  plycolemc  15472  rpcxpmul2  15627  lgsquad2lem2  15801  nninfsellemdc  16548  nnnninfex  16560