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  565  cbv1  1798  cbv1v  1800  ralimdaa  2616  reuss2  3513  finds2  4743  ssrel  4858  ssrel2  4860  ssrelrel  4870  funfvima2  5941  tfrlem1  6569  tfrlemi1  6593  tfr1onlemaccex  6609  tfrcllemaccex  6622  tfri3  6628  nneneq  7148  ac6sfi  7192  nnnninfeq  7458  nnnninfeq2  7459  pitonn  8205  nnaddcl  9303  nnmulcl  9304  zaddcllempos  9660  zaddcllemneg  9662  peano5uzti  9733  uzind2  9737  fzind  9740  zindd  9743  uzaddcl  9965  exfzdc  10637  frec2uzltd  10818  frecuzrdgg  10831  seq3val  10875  seqvalcd  10876  seq3clss  10886  monoord  10900  seq3caopr3  10906  seqcaopr3g  10907  seq3f1olemp  10930  seqf1oglem2a  10933  seqf1og  10936  seq3id3  10939  seq3homo  10942  seq3z  10943  seqfeq4g  10946  ser3ge0  10951  exp3vallem  10955  expcllem  10965  expap0  10984  mulexp  10993  expadd  10996  expmul  10999  leexp2r  11008  leexp1a  11009  bernneq  11076  modqexp  11082  nn0ltexp2  11125  apexp1  11134  facdiv  11154  facwordi  11156  faclbnd  11157  faclbnd6  11160  omgadd  11220  hashmap  11246  hashf1  11265  seq3coll  11272  cjexp  11636  resqrexlemover  11754  resqrexlemdecn  11756  resqrexlemlo  11757  resqrexlemcalc3  11760  absexp  11823  fsum2d  12180  modfsummod  12203  fsumabs  12210  fsumiun  12222  binom  12229  bcxmas  12234  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  clim2prod  12284  prodfap0  12290  prodfrecap  12291  fprodabs  12361  fprod2d  12368  demoivreALT  12519  dvdsfac  12605  bitsinv1  12707  gcdmultiple  12775  rplpwr  12782  nn0seqcvgd  12797  alginv  12803  algcvga  12807  algfx  12808  prmdvdsexp  12904  prmfac1  12908  eulerthlemrprm  12985  eulerthlema  12986  pcmpt  13100  pcfac  13107  prmpwdvds  13112  ennnfoneleminc  13280  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemhom  13284  nninfdclemlt  13320  mulgnnass  13937  mhmmulg  13943  gzsumconst  14120  srgmulgass  14267  srgpcomp  14268  lmodvsmmulgdi  14632  cnfldexp  14886  tgcl  15088  dvmptfsum  15749  plycolemc  15782  rpcxpmul2  15938  lgsquad2lem2  16115  eupth2lemsfi  16633  eupth2fi  16634  depindlem2  16662  depindlem3  16663  nninfsellemdc  16958  nnnninfex  16970