Theorem e333 16601

Description: A virtual deduction elimination rule.

Hypotheses

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

Assertion

Ref	Expression
e333	|- . ph, ps, ch   ⊢   ze .

Proof of Theorem e333

Step	Hyp	Ref	Expression
1		e333.1	. . . . . . . . . 10 |- . ph, ps, ch   ⊢   th .
2	1	dfvd3i 16496	. . . . . . . . 9 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 1061	. . . . . . . 8 |- ((ph /\ ps /\ ch) -> th)
4		e333.4	. . . . . . . 8 |- (th -> (ta -> (et -> ze)))
5	3, 4	syl 12	. . . . . . 7 |- ((ph /\ ps /\ ch) -> (ta -> (et -> ze)))
6		e333.2	. . . . . . . . 9 |- . ph, ps, ch   ⊢   ta .
7	6	dfvd3i 16496	. . . . . . . 8 |- (ph -> (ps -> (ch -> ta)))
8	7	3imp 1061	. . . . . . 7 |- ((ph /\ ps /\ ch) -> ta)
9	5, 8	syl5 20	. . . . . 6 |- ((ph /\ ps /\ ch) -> ((ph /\ ps /\ ch) -> (et -> ze)))
10	9	pm2.43i 78	. . . . 5 |- ((ph /\ ps /\ ch) -> (et -> ze))
11		e333.3	. . . . . . 7 |- . ph, ps, ch   ⊢   et .
12	11	dfvd3i 16496	. . . . . 6 |- (ph -> (ps -> (ch -> et)))
13	12	3imp 1061	. . . . 5 |- ((ph /\ ps /\ ch) -> et)
14	10, 13	syl5 20	. . . 4 |- ((ph /\ ps /\ ch) -> ((ph /\ ps /\ ch) -> ze))
15	14	pm2.43i 78	. . 3 |- ((ph /\ ps /\ ch) -> ze)
16	15	3exp 1066	. 2 |- (ph -> (ps -> (ch -> ze)))
17	16	dfvd3ir 16497	1 |- . ph, ps, ch   ⊢   ze .

Syntax hints:   -> wi 3   /\ w3a 858   . vd3 16493

This theorem is referenced by:  e33 16602  e123 16630

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  df-vd3 16494

Copyright terms: Public domain