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  2599  reuss2  3489  finds2  4705  ssrel  4820  ssrel2  4822  ssrelrel  4832  funfvima2  5897  tfrlem1  6517  tfrlemi1  6541  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfri3  6576  nneneq  7086  ac6sfi  7130  nnnninfeq  7370  nnnninfeq2  7371  pitonn  8111  nnaddcl  9205  nnmulcl  9206  zaddcllempos  9560  zaddcllemneg  9562  peano5uzti  9632  uzind2  9636  fzind  9639  zindd  9642  uzaddcl  9864  exfzdc  10532  frec2uzltd  10711  frecuzrdgg  10724  seq3val  10768  seqvalcd  10769  seq3clss  10779  monoord  10793  seq3caopr3  10799  seqcaopr3g  10800  seq3f1olemp  10823  seqf1oglem2a  10826  seqf1og  10829  seq3id3  10832  seq3homo  10835  seq3z  10836  seqfeq4g  10839  ser3ge0  10844  exp3vallem  10848  expcllem  10858  expap0  10877  mulexp  10886  expadd  10889  expmul  10892  leexp2r  10901  leexp1a  10902  bernneq  10968  modqexp  10974  nn0ltexp2  11017  apexp1  11026  facdiv  11046  facwordi  11048  faclbnd  11049  faclbnd6  11052  omgadd  11111  seq3coll  11152  cjexp  11516  resqrexlemover  11633  resqrexlemdecn  11635  resqrexlemlo  11636  resqrexlemcalc3  11639  absexp  11702  fsum2d  12059  modfsummod  12082  fsumabs  12089  fsumiun  12101  binom  12108  bcxmas  12113  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  clim2prod  12163  prodfap0  12169  prodfrecap  12170  fprodabs  12240  fprod2d  12247  demoivreALT  12398  dvdsfac  12484  bitsinv1  12586  gcdmultiple  12654  rplpwr  12661  nn0seqcvgd  12676  alginv  12682  algcvga  12686  algfx  12687  prmdvdsexp  12783  prmfac1  12787  eulerthlemrprm  12864  eulerthlema  12865  pcmpt  12979  pcfac  12986  prmpwdvds  12991  ennnfoneleminc  13095  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemhom  13099  nninfdclemlt  13135  gsumfzz  13641  mulgnnass  13807  mhmmulg  13813  gsumfzconst  13991  srgmulgass  14066  srgpcomp  14067  lmodvsmmulgdi  14402  cnfldexp  14656  gsumfzfsumlemm  14666  tgcl  14858  dvmptfsum  15519  plycolemc  15552  rpcxpmul2  15707  lgsquad2lem2  15884  eupth2lemsfi  16402  eupth2fi  16403  depindlem2  16431  depindlem3  16432  nninfsellemdc  16719  nnnninfex  16731