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  549  cbv1  1723  ralimdaa  2501  reuss2  3361  finds2  4523  ssrel  4635  ssrel2  4637  ssrelrel  4647  funfvima2  5658  tfrlem1  6213  tfrlemi1  6237  tfr1onlemaccex  6253  tfrcllemaccex  6266  tfri3  6272  nneneq  6759  ac6sfi  6800  pitonn  7680  nnaddcl  8764  nnmulcl  8765  zaddcllempos  9115  zaddcllemneg  9117  peano5uzti  9183  uzind2  9187  fzind  9190  zindd  9193  uzaddcl  9408  exfzdc  10048  frec2uzltd  10207  frecuzrdgg  10220  seq3val  10262  seqvalcd  10263  seq3clss  10271  monoord  10280  seq3caopr3  10285  seq3f1olemp  10306  seq3id3  10311  seq3homo  10314  seq3z  10315  ser3ge0  10321  exp3vallem  10325  expcllem  10335  expap0  10354  mulexp  10363  expadd  10366  expmul  10369  leexp2r  10378  leexp1a  10379  bernneq  10443  apexp1  10496  facdiv  10516  facwordi  10518  faclbnd  10519  faclbnd6  10522  omgadd  10580  seq3coll  10617  cjexp  10697  resqrexlemover  10814  resqrexlemdecn  10816  resqrexlemlo  10817  resqrexlemcalc3  10820  absexp  10883  fsum2d  11236  modfsummod  11259  fsumabs  11266  fsumiun  11278  binom  11285  bcxmas  11290  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  clim2prod  11340  prodfap0  11346  prodfrecap  11347  demoivreALT  11516  dvdsfac  11594  gcdmultiple  11744  rplpwr  11751  nn0seqcvgd  11758  alginv  11764  algcvga  11768  algfx  11769  prmdvdsexp  11862  prmfac1  11866  ennnfoneleminc  11960  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemhom  11964  tgcl  12272  nninfalllemn  13377  nninfsellemdc  13381