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  1759  cbv1v  1761  ralimdaa  2563  reuss2  3444  finds2  4638  ssrel  4752  ssrel2  4754  ssrelrel  4764  funfvima2  5798  tfrlem1  6375  tfrlemi1  6399  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfri3  6434  nneneq  6927  ac6sfi  6968  nnnninfeq  7203  nnnninfeq2  7204  pitonn  7932  nnaddcl  9027  nnmulcl  9028  zaddcllempos  9380  zaddcllemneg  9382  peano5uzti  9451  uzind2  9455  fzind  9458  zindd  9461  uzaddcl  9677  exfzdc  10333  frec2uzltd  10512  frecuzrdgg  10525  seq3val  10569  seqvalcd  10570  seq3clss  10580  monoord  10594  seq3caopr3  10600  seqcaopr3g  10601  seq3f1olemp  10624  seqf1oglem2a  10627  seqf1og  10630  seq3id3  10633  seq3homo  10636  seq3z  10637  seqfeq4g  10640  ser3ge0  10645  exp3vallem  10649  expcllem  10659  expap0  10678  mulexp  10687  expadd  10690  expmul  10693  leexp2r  10702  leexp1a  10703  bernneq  10769  modqexp  10775  nn0ltexp2  10818  apexp1  10827  facdiv  10847  facwordi  10849  faclbnd  10850  faclbnd6  10853  omgadd  10911  seq3coll  10951  cjexp  11075  resqrexlemover  11192  resqrexlemdecn  11194  resqrexlemlo  11195  resqrexlemcalc3  11198  absexp  11261  fsum2d  11617  modfsummod  11640  fsumabs  11647  fsumiun  11659  binom  11666  bcxmas  11671  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  clim2prod  11721  prodfap0  11727  prodfrecap  11728  fprodabs  11798  fprod2d  11805  demoivreALT  11956  dvdsfac  12042  bitsinv1  12144  gcdmultiple  12212  rplpwr  12219  nn0seqcvgd  12234  alginv  12240  algcvga  12244  algfx  12245  prmdvdsexp  12341  prmfac1  12345  eulerthlemrprm  12422  eulerthlema  12423  pcmpt  12537  pcfac  12544  prmpwdvds  12549  ennnfoneleminc  12653  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemhom  12657  nninfdclemlt  12693  gsumfzz  13197  mulgnnass  13363  mhmmulg  13369  gsumfzconst  13547  srgmulgass  13621  srgpcomp  13622  lmodvsmmulgdi  13955  cnfldexp  14209  gsumfzfsumlemm  14219  tgcl  14384  dvmptfsum  15045  plycolemc  15078  rpcxpmul2  15233  lgsquad2lem2  15407  nninfsellemdc  15741