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  4750  ssrel  4865  ssrel2  4867  ssrelrel  4877  funfvima2  5954  tfrlem1  6583  tfrlemi1  6607  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfri3  6642  nneneq  7162  ac6sfi  7206  nnnninfeq  7474  nnnninfeq2  7475  pitonn  8221  nnaddcl  9333  nnmulcl  9334  zaddcllempos  9692  zaddcllemneg  9694  peano5uzti  9765  uzind2  9769  fzind  9772  zindd  9775  uzaddcl  10002  exfzdc  10676  frec2uzltd  10861  frecuzrdgg  10874  seq3val  10918  seqvalcd  10919  seq3clss  10929  monoord  10943  seq3caopr3  10949  seqcaopr3g  10950  seq3f1olemp  10973  seqf1oglem2a  10976  seqf1og  10979  seq3id3  10982  seq3homo  10985  seq3z  10986  seqfeq4g  10989  ser3ge0  10994  exp3vallem  10998  expcllem  11008  expap0  11027  mulexp  11036  expadd  11039  expmul  11042  leexp2r  11051  leexp1a  11052  bernneq  11119  modqexp  11125  nn0ltexp2  11169  apexp1  11178  facdiv  11198  facwordi  11200  faclbnd  11201  faclbnd6  11204  omgadd  11264  hashmap  11290  hashf1  11309  seq3coll  11316  cjexp  11680  resqrexlemover  11798  resqrexlemdecn  11800  resqrexlemlo  11801  resqrexlemcalc3  11804  absexp  11868  fsum2d  12227  modfsummod  12250  fsumabs  12257  fsumiun  12269  binom  12276  bcxmas  12281  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  clim2prod  12331  prodfap0  12337  prodfrecap  12338  fprodabs  12408  fprod2d  12415  demoivreALT  12566  dvdsfac  12652  bitsinv1  12754  gcdmultiple  12822  rplpwr  12829  nn0seqcvgd  12844  alginv  12850  algcvga  12854  algfx  12855  prmdvdsexp  12952  prmfac1  12956  eulerthlemrprm  13036  eulerthlema  13037  pcmpt  13151  pcfac  13158  prmpwdvds  13163  ennnfoneleminc  13360  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemhom  13364  nninfdclemlt  13400  mulgnnass  14019  mhmmulg  14025  gzsumconst  14233  srgmulgass  14400  srgpcomp  14401  lmodvsmmulgdi  14769  cnfldexp  15023  assamulgscm  15152  tgcl  15290  dvmptfsum  15951  plycolemc  15984  rpcxpmul2  16146  bcmono  16304  bposlem5  16315  lgsquad2lem2  16406  eupth2lemsfi  16924  eupth2fi  16925  depindlem2  16953  depindlem3  16954  nninfsellemdc  17259  nnnninfex  17271