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 ) ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpdd  41  imim2d  54  imim3i  61  loowoz  103  animpimp2impd  565  cbv1  1798  cbv1v  1800  ralimdaa  2616  reuss2  3513  finds2  4748  ssrel  4863  ssrel2  4865  ssrelrel  4875  funfvima2  5951  tfrlem1  6579  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfri3  6638  nneneq  7158  ac6sfi  7202  nnnninfeq  7469  nnnninfeq2  7470  pitonn  8216  nnaddcl  9327  nnmulcl  9328  zaddcllempos  9686  zaddcllemneg  9688  peano5uzti  9759  uzind2  9763  fzind  9766  zindd  9769  uzaddcl  9996  exfzdc  10670  frec2uzltd  10855  frecuzrdgg  10868  seq3val  10912  seqvalcd  10913  seq3clss  10923  monoord  10937  seq3caopr3  10943  seqcaopr3g  10944  seq3f1olemp  10967  seqf1oglem2a  10970  seqf1og  10973  seq3id3  10976  seq3homo  10979  seq3z  10980  seqfeq4g  10983  ser3ge0  10988  exp3vallem  10992  expcllem  11002  expap0  11021  mulexp  11030  expadd  11033  expmul  11036  leexp2r  11045  leexp1a  11046  bernneq  11113  modqexp  11119  nn0ltexp2  11163  apexp1  11172  facdiv  11192  facwordi  11194  faclbnd  11195  faclbnd6  11198  omgadd  11258  hashmap  11284  hashf1  11303  seq3coll  11310  cjexp  11674  resqrexlemover  11792  resqrexlemdecn  11794  resqrexlemlo  11795  resqrexlemcalc3  11798  absexp  11862  fsum2d  12221  modfsummod  12244  fsumabs  12251  fsumiun  12263  binom  12270  bcxmas  12275  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  clim2prod  12325  prodfap0  12331  prodfrecap  12332  fprodabs  12402  fprod2d  12409  demoivreALT  12560  dvdsfac  12646  bitsinv1  12748  gcdmultiple  12816  rplpwr  12823  nn0seqcvgd  12838  alginv  12844  algcvga  12848  algfx  12849  prmdvdsexp  12946  prmfac1  12950  eulerthlemrprm  13030  eulerthlema  13031  pcmpt  13145  pcfac  13152  prmpwdvds  13157  ennnfoneleminc  13354  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemhom  13358  nninfdclemlt  13394  mulgnnass  14013  mhmmulg  14019  gzsumconst  14227  srgmulgass  14377  srgpcomp  14378  lmodvsmmulgdi  14744  cnfldexp  14998  assamulgscm  15127  tgcl  15256  dvmptfsum  15917  plycolemc  15950  rpcxpmul2  16110  bcmono  16265  bposlem5  16276  lgsquad2lem2  16367  eupth2lemsfi  16885  eupth2fi  16886  depindlem2  16914  depindlem3  16915  nninfsellemdc  17219  nnnninfex  17231