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  1767  cbv1v  1769  ralimdaa  2571  reuss2  3452  finds2  4648  ssrel  4762  ssrel2  4764  ssrelrel  4774  funfvima2  5816  tfrlem1  6393  tfrlemi1  6417  tfr1onlemaccex  6433  tfrcllemaccex  6446  tfri3  6452  nneneq  6953  ac6sfi  6994  nnnninfeq  7229  nnnninfeq2  7230  pitonn  7960  nnaddcl  9055  nnmulcl  9056  zaddcllempos  9408  zaddcllemneg  9410  peano5uzti  9480  uzind2  9484  fzind  9487  zindd  9490  uzaddcl  9706  exfzdc  10367  frec2uzltd  10546  frecuzrdgg  10559  seq3val  10603  seqvalcd  10604  seq3clss  10614  monoord  10628  seq3caopr3  10634  seqcaopr3g  10635  seq3f1olemp  10658  seqf1oglem2a  10661  seqf1og  10664  seq3id3  10667  seq3homo  10670  seq3z  10671  seqfeq4g  10674  ser3ge0  10679  exp3vallem  10683  expcllem  10693  expap0  10712  mulexp  10721  expadd  10724  expmul  10727  leexp2r  10736  leexp1a  10737  bernneq  10803  modqexp  10809  nn0ltexp2  10852  apexp1  10861  facdiv  10881  facwordi  10883  faclbnd  10884  faclbnd6  10887  omgadd  10945  seq3coll  10985  cjexp  11175  resqrexlemover  11292  resqrexlemdecn  11294  resqrexlemlo  11295  resqrexlemcalc3  11298  absexp  11361  fsum2d  11717  modfsummod  11740  fsumabs  11747  fsumiun  11759  binom  11766  bcxmas  11771  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  clim2prod  11821  prodfap0  11827  prodfrecap  11828  fprodabs  11898  fprod2d  11905  demoivreALT  12056  dvdsfac  12142  bitsinv1  12244  gcdmultiple  12312  rplpwr  12319  nn0seqcvgd  12334  alginv  12340  algcvga  12344  algfx  12345  prmdvdsexp  12441  prmfac1  12445  eulerthlemrprm  12522  eulerthlema  12523  pcmpt  12637  pcfac  12644  prmpwdvds  12649  ennnfoneleminc  12753  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemhom  12757  nninfdclemlt  12793  gsumfzz  13298  mulgnnass  13464  mhmmulg  13470  gsumfzconst  13648  srgmulgass  13722  srgpcomp  13723  lmodvsmmulgdi  14056  cnfldexp  14310  gsumfzfsumlemm  14320  tgcl  14507  dvmptfsum  15168  plycolemc  15201  rpcxpmul2  15356  lgsquad2lem2  15530  nninfsellemdc  15909  nnnninfex  15921