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 ) ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpdd  41  imim2d  54  imim3i  61  loowoz  103  animpimp2impd  565  cbv1  1798  cbv1v  1800  ralimdaa  2616  reuss2  3513  finds2  4750  ssrel  4865  ssrel2  4867  ssrelrel  4877  funfvima2  5954  tfrlem1  6584  tfrlemi1  6608  tfr1onlemaccex  6624  tfrcllemaccex  6637  tfri3  6643  nneneq  7164  ac6sfi  7208  nnnninfeq  7474  nnnninfeq2  7475  pitonn  8221  nnaddcl  9333  nnmulcl  9334  zaddcllempos  9690  zaddcllemneg  9692  peano5uzti  9764  uzind2  9768  fzind  9771  zindd  9774  uzaddcl  10001  exfzdc  10675  frec2uzltd  10860  frecuzrdgg  10873  seq3val  10917  seqvalcd  10918  seq3clss  10928  monoord  10942  seq3caopr3  10948  seqcaopr3g  10949  seq3f1olemp  10972  seqf1oglem2a  10975  seqf1og  10978  seq3id3  10981  seq3homo  10984  seq3z  10985  seqfeq4g  10988  ser3ge0  10993  exp3vallem  10997  expcllem  11007  expap0  11026  mulexp  11035  expadd  11038  expmul  11041  leexp2r  11050  leexp1a  11051  bernneq  11118  modqexp  11124  nn0ltexp2  11168  apexp1  11177  facdiv  11197  facwordi  11199  faclbnd  11200  faclbnd6  11203  omgadd  11263  hashmap  11289  hashf1  11308  seq3coll  11315  cjexp  11679  resqrexlemover  11797  resqrexlemdecn  11799  resqrexlemlo  11800  resqrexlemcalc3  11803  absexp  11867  fsum2d  12226  modfsummod  12249  fsumabs  12256  fsumiun  12268  binom  12275  bcxmas  12280  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  clim2prod  12330  prodfap0  12336  prodfrecap  12337  fprodabs  12407  fprod2d  12414  demoivreALT  12565  dvdsfac  12651  bitsinv1  12753  gcdmultiple  12821  rplpwr  12828  nn0seqcvgd  12843  alginv  12849  algcvga  12853  algfx  12854  prmdvdsexp  12951  prmfac1  12955  eulerthlemrprm  13035  eulerthlema  13036  pcmpt  13150  pcfac  13157  prmpwdvds  13162  ennnfoneleminc  13359  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemhom  13363  nninfdclemlt  13399  mulgnnass  14018  mhmmulg  14024  gzsumconst  14232  srgmulgass  14399  srgpcomp  14400  lmodvsmmulgdi  14768  cnfldexp  15022  assamulgscm  15151  tgcl  15307  dvmptfsum  15968  plycolemc  16001  rpcxpmul2  16163  bcmono  16321  bposlem5  16332  lgsquad2lem2  16423  eupth2lemsfi  16941  eupth2fi  16942  depindlem2  16970  depindlem3  16971  nninfsellemdc  17276  nnnninfex  17288