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  7468  nnnninfeq2  7469  pitonn  8215  nnaddcl  9324  nnmulcl  9325  zaddcllempos  9681  zaddcllemneg  9683  peano5uzti  9754  uzind2  9758  fzind  9761  zindd  9764  uzaddcl  9986  exfzdc  10659  frec2uzltd  10840  frecuzrdgg  10853  seq3val  10897  seqvalcd  10898  seq3clss  10908  monoord  10922  seq3caopr3  10928  seqcaopr3g  10929  seq3f1olemp  10952  seqf1oglem2a  10955  seqf1og  10958  seq3id3  10961  seq3homo  10964  seq3z  10965  seqfeq4g  10968  ser3ge0  10973  exp3vallem  10977  expcllem  10987  expap0  11006  mulexp  11015  expadd  11018  expmul  11021  leexp2r  11030  leexp1a  11031  bernneq  11098  modqexp  11104  nn0ltexp2  11147  apexp1  11156  facdiv  11176  facwordi  11178  faclbnd  11179  faclbnd6  11182  omgadd  11242  hashmap  11268  hashf1  11287  seq3coll  11294  cjexp  11658  resqrexlemover  11776  resqrexlemdecn  11778  resqrexlemlo  11779  resqrexlemcalc3  11782  absexp  11845  fsum2d  12202  modfsummod  12225  fsumabs  12232  fsumiun  12244  binom  12251  bcxmas  12256  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  clim2prod  12306  prodfap0  12312  prodfrecap  12313  fprodabs  12383  fprod2d  12390  demoivreALT  12541  dvdsfac  12627  bitsinv1  12729  gcdmultiple  12797  rplpwr  12804  nn0seqcvgd  12819  alginv  12825  algcvga  12829  algfx  12830  prmdvdsexp  12926  prmfac1  12930  eulerthlemrprm  13007  eulerthlema  13008  pcmpt  13122  pcfac  13129  prmpwdvds  13134  ennnfoneleminc  13302  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemhom  13306  nninfdclemlt  13342  mulgnnass  13960  mhmmulg  13966  gzsumconst  14143  srgmulgass  14293  srgpcomp  14294  lmodvsmmulgdi  14660  cnfldexp  14914  assamulgscm  15043  tgcl  15165  dvmptfsum  15826  plycolemc  15859  rpcxpmul2  16015  lgsquad2lem2  16201  eupth2lemsfi  16719  eupth2fi  16720  depindlem2  16748  depindlem3  16749  nninfsellemdc  17053  nnnninfex  17065