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  1768  cbv1v  1770  ralimdaa  2572  reuss2  3453  finds2  4649  ssrel  4763  ssrel2  4765  ssrelrel  4775  funfvima2  5817  tfrlem1  6394  tfrlemi1  6418  tfr1onlemaccex  6434  tfrcllemaccex  6447  tfri3  6453  nneneq  6954  ac6sfi  6995  nnnninfeq  7230  nnnninfeq2  7231  pitonn  7961  nnaddcl  9056  nnmulcl  9057  zaddcllempos  9409  zaddcllemneg  9411  peano5uzti  9481  uzind2  9485  fzind  9488  zindd  9491  uzaddcl  9707  exfzdc  10369  frec2uzltd  10548  frecuzrdgg  10561  seq3val  10605  seqvalcd  10606  seq3clss  10616  monoord  10630  seq3caopr3  10636  seqcaopr3g  10637  seq3f1olemp  10660  seqf1oglem2a  10663  seqf1og  10666  seq3id3  10669  seq3homo  10672  seq3z  10673  seqfeq4g  10676  ser3ge0  10681  exp3vallem  10685  expcllem  10695  expap0  10714  mulexp  10723  expadd  10726  expmul  10729  leexp2r  10738  leexp1a  10739  bernneq  10805  modqexp  10811  nn0ltexp2  10854  apexp1  10863  facdiv  10883  facwordi  10885  faclbnd  10886  faclbnd6  10889  omgadd  10947  seq3coll  10987  cjexp  11204  resqrexlemover  11321  resqrexlemdecn  11323  resqrexlemlo  11324  resqrexlemcalc3  11327  absexp  11390  fsum2d  11746  modfsummod  11769  fsumabs  11776  fsumiun  11788  binom  11795  bcxmas  11800  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  clim2prod  11850  prodfap0  11856  prodfrecap  11857  fprodabs  11927  fprod2d  11934  demoivreALT  12085  dvdsfac  12171  bitsinv1  12273  gcdmultiple  12341  rplpwr  12348  nn0seqcvgd  12363  alginv  12369  algcvga  12373  algfx  12374  prmdvdsexp  12470  prmfac1  12474  eulerthlemrprm  12551  eulerthlema  12552  pcmpt  12666  pcfac  12673  prmpwdvds  12678  ennnfoneleminc  12782  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemhom  12786  nninfdclemlt  12822  gsumfzz  13327  mulgnnass  13493  mhmmulg  13499  gsumfzconst  13677  srgmulgass  13751  srgpcomp  13752  lmodvsmmulgdi  14085  cnfldexp  14339  gsumfzfsumlemm  14349  tgcl  14536  dvmptfsum  15197  plycolemc  15230  rpcxpmul2  15385  lgsquad2lem2  15559  nninfsellemdc  15947  nnnninfex  15959