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  1743  cbv1v  1745  ralimdaa  2541  reuss2  3413  finds2  4594  ssrel  4708  ssrel2  4710  ssrelrel  4720  funfvima2  5740  tfrlem1  6299  tfrlemi1  6323  tfr1onlemaccex  6339  tfrcllemaccex  6352  tfri3  6358  nneneq  6847  ac6sfi  6888  nnnninfeq  7116  nnnninfeq2  7117  pitonn  7822  nnaddcl  8912  nnmulcl  8913  zaddcllempos  9263  zaddcllemneg  9265  peano5uzti  9334  uzind2  9338  fzind  9341  zindd  9344  uzaddcl  9559  exfzdc  10210  frec2uzltd  10373  frecuzrdgg  10386  seq3val  10428  seqvalcd  10429  seq3clss  10437  monoord  10446  seq3caopr3  10451  seq3f1olemp  10472  seq3id3  10477  seq3homo  10480  seq3z  10481  ser3ge0  10487  exp3vallem  10491  expcllem  10501  expap0  10520  mulexp  10529  expadd  10532  expmul  10535  leexp2r  10544  leexp1a  10545  bernneq  10610  modqexp  10616  nn0ltexp2  10658  apexp1  10666  facdiv  10686  facwordi  10688  faclbnd  10689  faclbnd6  10692  omgadd  10750  seq3coll  10790  cjexp  10870  resqrexlemover  10987  resqrexlemdecn  10989  resqrexlemlo  10990  resqrexlemcalc3  10993  absexp  11056  fsum2d  11411  modfsummod  11434  fsumabs  11441  fsumiun  11453  binom  11460  bcxmas  11465  cvgratnnlemnexp  11500  cvgratnnlemmn  11501  clim2prod  11515  prodfap0  11521  prodfrecap  11522  fprodabs  11592  fprod2d  11599  demoivreALT  11749  dvdsfac  11833  gcdmultiple  11988  rplpwr  11995  nn0seqcvgd  12008  alginv  12014  algcvga  12018  algfx  12019  prmdvdsexp  12115  prmfac1  12119  eulerthlemrprm  12196  eulerthlema  12197  pcmpt  12308  pcfac  12315  prmpwdvds  12320  ennnfoneleminc  12379  ennnfonelemkh  12380  ennnfonelemhf1o  12381  ennnfonelemhom  12383  nninfdclemlt  12419  mulgnnass  12878  mhmmulg  12884  srgmulgass  12969  srgpcomp  12970  tgcl  13135  nninfsellemdc  14320