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  103  animpimp2impd  559  cbv1  1769  cbv1v  1771  ralimdaa  2573  reuss2  3457  finds2  4662  ssrel  4776  ssrel2  4778  ssrelrel  4788  funfvima2  5835  tfrlem1  6412  tfrlemi1  6436  tfr1onlemaccex  6452  tfrcllemaccex  6465  tfri3  6471  nneneq  6974  ac6sfi  7016  nnnninfeq  7251  nnnninfeq2  7252  pitonn  7991  nnaddcl  9086  nnmulcl  9087  zaddcllempos  9439  zaddcllemneg  9441  peano5uzti  9511  uzind2  9515  fzind  9518  zindd  9521  uzaddcl  9737  exfzdc  10401  frec2uzltd  10580  frecuzrdgg  10593  seq3val  10637  seqvalcd  10638  seq3clss  10648  monoord  10662  seq3caopr3  10668  seqcaopr3g  10669  seq3f1olemp  10692  seqf1oglem2a  10695  seqf1og  10698  seq3id3  10701  seq3homo  10704  seq3z  10705  seqfeq4g  10708  ser3ge0  10713  exp3vallem  10717  expcllem  10727  expap0  10746  mulexp  10755  expadd  10758  expmul  10761  leexp2r  10770  leexp1a  10771  bernneq  10837  modqexp  10843  nn0ltexp2  10886  apexp1  10895  facdiv  10915  facwordi  10917  faclbnd  10918  faclbnd6  10921  omgadd  10979  seq3coll  11019  cjexp  11289  resqrexlemover  11406  resqrexlemdecn  11408  resqrexlemlo  11409  resqrexlemcalc3  11412  absexp  11475  fsum2d  11831  modfsummod  11854  fsumabs  11861  fsumiun  11873  binom  11880  bcxmas  11885  cvgratnnlemnexp  11920  cvgratnnlemmn  11921  clim2prod  11935  prodfap0  11941  prodfrecap  11942  fprodabs  12012  fprod2d  12019  demoivreALT  12170  dvdsfac  12256  bitsinv1  12358  gcdmultiple  12426  rplpwr  12433  nn0seqcvgd  12448  alginv  12454  algcvga  12458  algfx  12459  prmdvdsexp  12555  prmfac1  12559  eulerthlemrprm  12636  eulerthlema  12637  pcmpt  12751  pcfac  12758  prmpwdvds  12763  ennnfoneleminc  12867  ennnfonelemkh  12868  ennnfonelemhf1o  12869  ennnfonelemhom  12871  nninfdclemlt  12907  gsumfzz  13412  mulgnnass  13578  mhmmulg  13584  gsumfzconst  13762  srgmulgass  13836  srgpcomp  13837  lmodvsmmulgdi  14170  cnfldexp  14424  gsumfzfsumlemm  14434  tgcl  14621  dvmptfsum  15282  plycolemc  15315  rpcxpmul2  15470  lgsquad2lem2  15644  nninfsellemdc  16119  nnnninfex  16131