Theorem e22 16561

Description: A virtual deduction elimination rule.

Hypotheses

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

Assertion

Ref	Expression
e22	|- . ph, ps   ⊢   ta .

Proof of Theorem e22

Step	Hyp	Ref	Expression
1		e22.1	. 2 |- . ph, ps   ⊢   ch .
2		e22.2	. 2 |- . ph, ps   ⊢   th .
3		e22.3	. . 3 |- (ch -> (th -> ta))
4	3	a1i 8	. 2 |- (ch -> (ch -> (th -> ta)))
5	1, 1, 2, 4	e222 16526	1 |- . ph, ps   ⊢   ta .

Syntax hints:   -> wi 3   . vd2 16488

This theorem is referenced by:  e22an 16562  e02 16589  e12 16593  e20 16595  e21 16598  sspwtr 16643  pwtrVD 16646  pwtrrVD 16648  elex22VD 16663  tpid3gVD 16666  en3lplem2VD 16668  imbi12VD 16697  truniALTVD 16702  trintALTVD 16704

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