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  561  cbv1  1793  cbv1v  1795  ralimdaa  2598  reuss2  3487  finds2  4699  ssrel  4814  ssrel2  4816  ssrelrel  4826  funfvima2  5886  tfrlem1  6473  tfrlemi1  6497  tfr1onlemaccex  6513  tfrcllemaccex  6526  tfri3  6532  nneneq  7042  ac6sfi  7086  nnnninfeq  7326  nnnninfeq2  7327  pitonn  8067  nnaddcl  9162  nnmulcl  9163  zaddcllempos  9515  zaddcllemneg  9517  peano5uzti  9587  uzind2  9591  fzind  9594  zindd  9597  uzaddcl  9819  exfzdc  10485  frec2uzltd  10664  frecuzrdgg  10677  seq3val  10721  seqvalcd  10722  seq3clss  10732  monoord  10746  seq3caopr3  10752  seqcaopr3g  10753  seq3f1olemp  10776  seqf1oglem2a  10779  seqf1og  10782  seq3id3  10785  seq3homo  10788  seq3z  10789  seqfeq4g  10792  ser3ge0  10797  exp3vallem  10801  expcllem  10811  expap0  10830  mulexp  10839  expadd  10842  expmul  10845  leexp2r  10854  leexp1a  10855  bernneq  10921  modqexp  10927  nn0ltexp2  10970  apexp1  10979  facdiv  10999  facwordi  11001  faclbnd  11002  faclbnd6  11005  omgadd  11064  seq3coll  11105  cjexp  11453  resqrexlemover  11570  resqrexlemdecn  11572  resqrexlemlo  11573  resqrexlemcalc3  11576  absexp  11639  fsum2d  11995  modfsummod  12018  fsumabs  12025  fsumiun  12037  binom  12044  bcxmas  12049  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  clim2prod  12099  prodfap0  12105  prodfrecap  12106  fprodabs  12176  fprod2d  12183  demoivreALT  12334  dvdsfac  12420  bitsinv1  12522  gcdmultiple  12590  rplpwr  12597  nn0seqcvgd  12612  alginv  12618  algcvga  12622  algfx  12623  prmdvdsexp  12719  prmfac1  12723  eulerthlemrprm  12800  eulerthlema  12801  pcmpt  12915  pcfac  12922  prmpwdvds  12927  ennnfoneleminc  13031  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemhom  13035  nninfdclemlt  13071  gsumfzz  13577  mulgnnass  13743  mhmmulg  13749  gsumfzconst  13927  srgmulgass  14001  srgpcomp  14002  lmodvsmmulgdi  14336  cnfldexp  14590  gsumfzfsumlemm  14600  tgcl  14787  dvmptfsum  15448  plycolemc  15481  rpcxpmul2  15636  lgsquad2lem2  15810  nninfsellemdc  16612  nnnninfex  16624