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 1417  ssralv 2110  poss 2836  soss 2847  frss 2916  dfwe2 2930  tfi 3121  funss 3526  abianfp 3953  nneneq 4498  abfii4 4544  axpowndlem3 4931  indpi 5014  suplem1pr 5141  pre-axsup 5271  fsequb 6463  seqzfveq 6494  cau5i 6862  cau4i 6863  cau5 6864  cvg1i 6865  cvg3 6868  fsumcllem 6960  fsum1ps 6964  fsumsplit 6966  fsumadd 6968  fsumcom 6974  fsumrev 6975  fsummulc1 6979  fsumcmp 6986  fsumcmpndx2 6988  fsumabs 6989  clm4 7026  clim2serzt 7078  caucvglem6 7106  isum1p 7149  iserzgt0 7154  expcnvlem1 7170  fsum0diaglem2 7200  fsum0diag2 7202  fsum0diag3 7203  fsum0diag4 7204  elcls3 7661  xplm 7925  occont 9099  occllem6 9117  mdslmd1lem1 10189  ismonc 10620  icmpmon 10623

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

Copyright terms: Public domain