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  4748  ssrel  4863  ssrel2  4865  ssrelrel  4875  funfvima2  5951  tfrlem1  6579  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfri3  6638  nneneq  7158  ac6sfi  7202  nnnninfeq  7468  nnnninfeq2  7469  pitonn  8215  nnaddcl  9326  nnmulcl  9327  zaddcllempos  9685  zaddcllemneg  9687  peano5uzti  9758  uzind2  9762  fzind  9765  zindd  9768  uzaddcl  9995  exfzdc  10669  frec2uzltd  10853  frecuzrdgg  10866  seq3val  10910  seqvalcd  10911  seq3clss  10921  monoord  10935  seq3caopr3  10941  seqcaopr3g  10942  seq3f1olemp  10965  seqf1oglem2a  10968  seqf1og  10971  seq3id3  10974  seq3homo  10977  seq3z  10978  seqfeq4g  10981  ser3ge0  10986  exp3vallem  10990  expcllem  11000  expap0  11019  mulexp  11028  expadd  11031  expmul  11034  leexp2r  11043  leexp1a  11044  bernneq  11111  modqexp  11117  nn0ltexp2  11161  apexp1  11170  facdiv  11190  facwordi  11192  faclbnd  11193  faclbnd6  11196  omgadd  11256  hashmap  11282  hashf1  11301  seq3coll  11308  cjexp  11672  resqrexlemover  11790  resqrexlemdecn  11792  resqrexlemlo  11793  resqrexlemcalc3  11796  absexp  11860  fsum2d  12218  modfsummod  12241  fsumabs  12248  fsumiun  12260  binom  12267  bcxmas  12272  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  clim2prod  12322  prodfap0  12328  prodfrecap  12329  fprodabs  12399  fprod2d  12406  demoivreALT  12557  dvdsfac  12643  bitsinv1  12745  gcdmultiple  12813  rplpwr  12820  nn0seqcvgd  12835  alginv  12841  algcvga  12845  algfx  12846  prmdvdsexp  12943  prmfac1  12947  eulerthlemrprm  13027  eulerthlema  13028  pcmpt  13142  pcfac  13149  prmpwdvds  13154  ennnfoneleminc  13351  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemhom  13355  nninfdclemlt  13391  mulgnnass  14009  mhmmulg  14015  gzsumconst  14192  srgmulgass  14342  srgpcomp  14343  lmodvsmmulgdi  14709  cnfldexp  14963  assamulgscm  15092  tgcl  15214  dvmptfsum  15875  plycolemc  15908  rpcxpmul2  16068  bcmono  16202  bposlem5  16213  lgsquad2lem2  16299  eupth2lemsfi  16817  eupth2fi  16818  depindlem2  16846  depindlem3  16847  nninfsellemdc  17151  nnnninfex  17163