Theorem e222 16526

Description: A virtual deduction elimination rule.

Hypotheses

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

Assertion

Ref	Expression
e222	|- . ph, ps   ⊢   et .

Proof of Theorem e222

Step	Hyp	Ref	Expression
1		e222.1	. . . . . . . . . 10 |- . ph, ps   ⊢   ch .
2	1	dfvd2i 16491	. . . . . . . . 9 |- (ph -> (ps -> ch))
3	2	imp 377	. . . . . . . 8 |- ((ph /\ ps) -> ch)
4		e222.4	. . . . . . . 8 |- (ch -> (th -> (ta -> et)))
5	3, 4	syl 12	. . . . . . 7 |- ((ph /\ ps) -> (th -> (ta -> et)))
6		e222.2	. . . . . . . . 9 |- . ph, ps   ⊢   th .
7	6	dfvd2i 16491	. . . . . . . 8 |- (ph -> (ps -> th))
8	7	imp 377	. . . . . . 7 |- ((ph /\ ps) -> th)
9	5, 8	syl5 20	. . . . . 6 |- ((ph /\ ps) -> ((ph /\ ps) -> (ta -> et)))
10	9	pm2.43i 78	. . . . 5 |- ((ph /\ ps) -> (ta -> et))
11		e222.3	. . . . . . 7 |- . ph, ps   ⊢   ta .
12	11	dfvd2i 16491	. . . . . 6 |- (ph -> (ps -> ta))
13	12	imp 377	. . . . 5 |- ((ph /\ ps) -> ta)
14	10, 13	syl5 20	. . . 4 |- ((ph /\ ps) -> ((ph /\ ps) -> et))
15	14	pm2.43i 78	. . 3 |- ((ph /\ ps) -> et)
16	15	ex 402	. 2 |- (ph -> (ps -> et))
17	16	dfvd2ir 16492	1 |- . ph, ps   ⊢   et .

Syntax hints:   -> wi 3   /\ wa 240   . vd2 16488

This theorem is referenced by:  e220 16527  e202 16529  e022 16531  e002 16533  e020 16535  e200 16537  e221 16539  e212 16541  e122 16543  e112 16544  e121 16546  e211 16547  e22 16561  suctrALT2VD 16660  en3lplem2VD 16668  19.21a3con13vVD 16676  tratrbVD 16685

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-vd2 16489

Copyright terms: Public domain