Theorem ee333 1279

Description: e333 16601 without virtual deductions.

Hypotheses

Ref	Expression
ee333.1	|- (ph -> (ps -> (ch -> th)))
ee333.2	|- (ph -> (ps -> (ch -> ta)))
ee333.3	|- (ph -> (ps -> (ch -> et)))
ee333.4	|- (th -> (ta -> (et -> ze)))

Assertion

Ref	Expression
ee333	|- (ph -> (ps -> (ch -> ze)))

Proof of Theorem ee333

Step	Hyp	Ref	Expression
1		ee333.3	. . . 4 |- (ph -> (ps -> (ch -> et)))
2	1	3imp 1061	. . 3 |- ((ph /\ ps /\ ch) -> et)
3		ee333.1	. . . . 5 |- (ph -> (ps -> (ch -> th)))
4	3	3imp 1061	. . . 4 |- ((ph /\ ps /\ ch) -> th)
5		ee333.2	. . . . 5 |- (ph -> (ps -> (ch -> ta)))
6	5	3imp 1061	. . . 4 |- ((ph /\ ps /\ ch) -> ta)
7		ee333.4	. . . 4 |- (th -> (ta -> (et -> ze)))
8	4, 6, 7	sylc 83	. . 3 |- ((ph /\ ps /\ ch) -> (et -> ze))
9	2, 8	mpd 29	. 2 |- ((ph /\ ps /\ ch) -> ze)
10	9	3exp 1066	1 |- (ph -> (ps -> (ch -> ze)))

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  ee323 1280  ee123 16631

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain