Theorem syl4d 28

Description: Deduction adding nested consequents.

Hypothesis

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

Assertion

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

Proof of Theorem syl4d

Step	Hyp	Ref	Expression
1		syl4d.1	. 2 |- (ph -> (ps -> ch))
2		syl2 17	. 2 |- ((ps -> ch) -> ((ch -> th) -> (ps -> th)))
3	1, 2	syl 12	1 |- (ph -> ((ch -> th) -> (ps -> th)))

Syntax hints:   -> wi 2

This theorem is referenced by:  syl34d 29  syl5d 53  expt 123  del43 856  moimv 1044  poss 2129  soss 2140  frss 2173  dfwe2 2187  tfi 2244  funss 2682  abianfp 3000  nneneq 3408  axpowndlem3 3745  indpi 3828  suplem1pr 3955  axsup 4088  occont 5168  occllem6 5185  mdbr3 5729  mdbr4 5730

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org