Theorem imim1d 28

Description: Deduction adding nested consequents.

Hypothesis

Ref	Expression
imim1d.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
imim1d	|- (ph -> ((ch -> th) -> (ps -> th)))

Proof of Theorem imim1d

Step	Hyp	Ref	Expression
1		imim1d.1	. 2 |- (ph -> (ps -> ch))
2		imim1 15	. 2 |- ((ps -> ch) -> ((ch -> th) -> (ps -> th)))
3	1, 2	syl 10	1 |- (ph -> ((ch -> th) -> (ps -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  imim12d 29  pm2.37OLD 99  pm2.61 124  expt 142  pm3.37 286  moimv 1419  ssralv 2112  poss 2838  soss 2849  frss 2918  dfwe2 2932  tfi 3123  funss 3531  abianfp 3959  nneneq 4505  abfii4 4551  axpowndlem3 4938  indpi 5021  suplem1pr 5148  pre-axsup 5278  fsequb 6473  seqzfveq 6504  cau5i 6883  cau4i 6884  cau5 6885  cvg1i 6886  cvg3 6889  fsumcllem 6982  fsum1ps 6986  fsumsplit 6988  fsumadd 6990  fsumcom 6996  fsumrev 6997  fsummulc1 7001  fsumcmp 7008  fsumcmpndx2 7010  fsumabs 7011  clm4 7048  clim2serzt 7103  caucvglem6 7131  isum1p 7177  iserzgt0 7182  expcnvlem1 7198  fsum0diaglem2 7228  fsum0diag2 7230  fsum0diag3 7231  fsum0diag4 7232  elcls3 7690  xplm 7958  occont 9148  occllem6 9166  mdslmd1lem1 10243  ismonc 10691  icmpmon 10694

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain