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  1794  cbv1v  1796  ralimdaa  2610  reuss2  3505  finds2  4728  ssrel  4843  ssrel2  4845  ssrelrel  4855  funfvima2  5924  tfrlem1  6552  tfrlemi1  6576  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfri3  6611  nneneq  7124  ac6sfi  7168  nnnninfeq  7432  nnnninfeq2  7433  pitonn  8179  nnaddcl  9274  nnmulcl  9275  zaddcllempos  9631  zaddcllemneg  9633  peano5uzti  9704  uzind2  9708  fzind  9711  zindd  9714  uzaddcl  9936  exfzdc  10608  frec2uzltd  10789  frecuzrdgg  10802  seq3val  10846  seqvalcd  10847  seq3clss  10857  monoord  10871  seq3caopr3  10877  seqcaopr3g  10878  seq3f1olemp  10901  seqf1oglem2a  10904  seqf1og  10907  seq3id3  10910  seq3homo  10913  seq3z  10914  seqfeq4g  10917  ser3ge0  10922  exp3vallem  10926  expcllem  10936  expap0  10955  mulexp  10964  expadd  10967  expmul  10970  leexp2r  10979  leexp1a  10980  bernneq  11047  modqexp  11053  nn0ltexp2  11096  apexp1  11105  facdiv  11125  facwordi  11127  faclbnd  11128  faclbnd6  11131  omgadd  11191  hashmap  11217  seq3coll  11239  cjexp  11603  resqrexlemover  11720  resqrexlemdecn  11722  resqrexlemlo  11723  resqrexlemcalc3  11726  absexp  11789  fsum2d  12146  modfsummod  12169  fsumabs  12176  fsumiun  12188  binom  12195  bcxmas  12200  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  clim2prod  12250  prodfap0  12256  prodfrecap  12257  fprodabs  12327  fprod2d  12334  demoivreALT  12485  dvdsfac  12571  bitsinv1  12673  gcdmultiple  12741  rplpwr  12748  nn0seqcvgd  12763  alginv  12769  algcvga  12773  algfx  12774  prmdvdsexp  12870  prmfac1  12874  eulerthlemrprm  12951  eulerthlema  12952  pcmpt  13066  pcfac  13073  prmpwdvds  13078  ennnfoneleminc  13246  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemhom  13250  nninfdclemlt  13286  gsumfzz  13750  mulgnnass  13910  mhmmulg  13916  gsumfzconst  14094  srgmulgass  14232  srgpcomp  14233  lmodvsmmulgdi  14597  cnfldexp  14851  gsumfzfsumlemm  14861  tgcl  15055  dvmptfsum  15716  plycolemc  15749  rpcxpmul2  15904  lgsquad2lem2  16081  eupth2lemsfi  16599  eupth2fi  16600  depindlem2  16628  depindlem3  16629  nninfsellemdc  16914  nnnninfex  16926