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  102  animpimp2impd  555  cbv1  1739  cbv1v  1741  ralimdaa  2537  reuss2  3408  finds2  4586  ssrel  4700  ssrel2  4702  ssrelrel  4712  funfvima2  5732  tfrlem1  6291  tfrlemi1  6315  tfr1onlemaccex  6331  tfrcllemaccex  6344  tfri3  6350  nneneq  6839  ac6sfi  6880  nnnninfeq  7108  nnnninfeq2  7109  pitonn  7814  nnaddcl  8902  nnmulcl  8903  zaddcllempos  9253  zaddcllemneg  9255  peano5uzti  9324  uzind2  9328  fzind  9331  zindd  9334  uzaddcl  9549  exfzdc  10200  frec2uzltd  10363  frecuzrdgg  10376  seq3val  10418  seqvalcd  10419  seq3clss  10427  monoord  10436  seq3caopr3  10441  seq3f1olemp  10462  seq3id3  10467  seq3homo  10470  seq3z  10471  ser3ge0  10477  exp3vallem  10481  expcllem  10491  expap0  10510  mulexp  10519  expadd  10522  expmul  10525  leexp2r  10534  leexp1a  10535  bernneq  10600  modqexp  10606  nn0ltexp2  10648  apexp1  10656  facdiv  10676  facwordi  10678  faclbnd  10679  faclbnd6  10682  omgadd  10741  seq3coll  10781  cjexp  10861  resqrexlemover  10978  resqrexlemdecn  10980  resqrexlemlo  10981  resqrexlemcalc3  10984  absexp  11047  fsum2d  11402  modfsummod  11425  fsumabs  11432  fsumiun  11444  binom  11451  bcxmas  11456  cvgratnnlemnexp  11491  cvgratnnlemmn  11492  clim2prod  11506  prodfap0  11512  prodfrecap  11513  fprodabs  11583  fprod2d  11590  demoivreALT  11740  dvdsfac  11824  gcdmultiple  11979  rplpwr  11986  nn0seqcvgd  11999  alginv  12005  algcvga  12009  algfx  12010  prmdvdsexp  12106  prmfac1  12110  eulerthlemrprm  12187  eulerthlema  12188  pcmpt  12299  pcfac  12306  prmpwdvds  12311  ennnfoneleminc  12370  ennnfonelemkh  12371  ennnfonelemhf1o  12372  ennnfonelemhom  12374  nninfdclemlt  12410  mulgnnass  12850  mhmmulg  12856  tgcl  12943  nninfsellemdc  14128