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 1412  ssralv 2104  poss 2832  soss 2843  frss 2911  dfwe2 2925  tfi 3116  funss 3520  abianfp 3947  nneneq 4492  abfii4 4538  axpowndlem3 4923  indpi 5006  suplem1pr 5133  pre-axsup 5263  fsequb 6455  seqzfveq 6486  cau5i 6854  cau4i 6855  cau5 6856  cvg1i 6857  cvg3 6860  fsumcllem 6952  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  fsumcom 6966  fsumrev 6967  fsummulc1 6971  fsumcmp 6978  fsumcmpndx2 6980  fsumabs 6981  clm4 7018  clim2serzt 7070  caucvglem6 7098  isum1p 7141  iserzgt0 7146  expcnvlem1 7162  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag3 7195  fsum0diag4 7196  elcls3 7652  xplm 7909  occont 9076  occllem6 9094  mdslmd1lem1 10160  ismonc 10584  icmpmon 10587

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

Copyright terms: Public domain