Theorem e111 16564

Description: A virtual deduction elimination rule.

Hypotheses

Ref	Expression
e111.1	|- . ph   ⊢   ps .
e111.2	|- . ph   ⊢   ch .
e111.3	|- . ph   ⊢   th .
e111.4	|- (ps -> (ch -> (th -> ta)))

Assertion

Ref	Expression
e111	|- . ph   ⊢   ta .

Proof of Theorem e111

Step	Hyp	Ref	Expression
1		e111.1	. . . . . . . 8 |- . ph   ⊢   ps .
2	1	in1 16481	. . . . . . 7 |- (ph -> ps)
3		e111.4	. . . . . . 7 |- (ps -> (ch -> (th -> ta)))
4	2, 3	syl 12	. . . . . 6 |- (ph -> (ch -> (th -> ta)))
5		e111.2	. . . . . . 7 |- . ph   ⊢   ch .
6	5	in1 16481	. . . . . 6 |- (ph -> ch)
7	4, 6	syl5 20	. . . . 5 |- (ph -> (ph -> (th -> ta)))
8	7	pm2.43i 78	. . . 4 |- (ph -> (th -> ta))
9		e111.3	. . . . 5 |- . ph   ⊢   th .
10	9	in1 16481	. . . 4 |- (ph -> th)
11	8, 10	syl5 20	. . 3 |- (ph -> (ph -> ta))
12	11	pm2.43i 78	. 2 |- (ph -> ta)
13	12	dfvd1ir 16483	1 |- . ph   ⊢   ta .

Syntax hints:   -> wi 3   . vd1 16479

This theorem is referenced by:  e110 16566  e101 16568  e011 16570  e100 16572  e010 16574  e001 16576  e11 16578  sbcoreleleqVD 16683  ordelordaxrVD 16691

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-vd1 16480

Copyright terms: Public domain