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  561  cbv1  1793  cbv1v  1795  ralimdaa  2598  reuss2  3487  finds2  4699  ssrel  4814  ssrel2  4816  ssrelrel  4826  funfvima2  5887  tfrlem1  6474  tfrlemi1  6498  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfri3  6533  nneneq  7043  ac6sfi  7087  nnnninfeq  7327  nnnninfeq2  7328  pitonn  8068  nnaddcl  9163  nnmulcl  9164  zaddcllempos  9516  zaddcllemneg  9518  peano5uzti  9588  uzind2  9592  fzind  9595  zindd  9598  uzaddcl  9820  exfzdc  10487  frec2uzltd  10666  frecuzrdgg  10679  seq3val  10723  seqvalcd  10724  seq3clss  10734  monoord  10748  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemp  10778  seqf1oglem2a  10781  seqf1og  10784  seq3id3  10787  seq3homo  10790  seq3z  10791  seqfeq4g  10794  ser3ge0  10799  exp3vallem  10803  expcllem  10813  expap0  10832  mulexp  10841  expadd  10844  expmul  10847  leexp2r  10856  leexp1a  10857  bernneq  10923  modqexp  10929  nn0ltexp2  10972  apexp1  10981  facdiv  11001  facwordi  11003  faclbnd  11004  faclbnd6  11007  omgadd  11066  seq3coll  11107  cjexp  11471  resqrexlemover  11588  resqrexlemdecn  11590  resqrexlemlo  11591  resqrexlemcalc3  11594  absexp  11657  fsum2d  12014  modfsummod  12037  fsumabs  12044  fsumiun  12056  binom  12063  bcxmas  12068  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  clim2prod  12118  prodfap0  12124  prodfrecap  12125  fprodabs  12195  fprod2d  12202  demoivreALT  12353  dvdsfac  12439  bitsinv1  12541  gcdmultiple  12609  rplpwr  12616  nn0seqcvgd  12631  alginv  12637  algcvga  12641  algfx  12642  prmdvdsexp  12738  prmfac1  12742  eulerthlemrprm  12819  eulerthlema  12820  pcmpt  12934  pcfac  12941  prmpwdvds  12946  ennnfoneleminc  13050  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemhom  13054  nninfdclemlt  13090  gsumfzz  13596  mulgnnass  13762  mhmmulg  13768  gsumfzconst  13946  srgmulgass  14021  srgpcomp  14022  lmodvsmmulgdi  14356  cnfldexp  14610  gsumfzfsumlemm  14620  tgcl  14807  dvmptfsum  15468  plycolemc  15501  rpcxpmul2  15656  lgsquad2lem2  15830  eupth2lemsfi  16348  eupth2fi  16349  depindlem2  16377  depindlem3  16378  nninfsellemdc  16663  nnnninfex  16675