Theorem e11 16578

Description: A virtual deduction elimination rule.

Hypotheses

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

Assertion

Ref	Expression
e11	|- . ph   ⊢   th .

Proof of Theorem e11

Step	Hyp	Ref	Expression
1		e11.1	. 2 |- . ph   ⊢   ps .
2		e11.2	. 2 |- . ph   ⊢   ch .
3		e11.3	. . 3 |- (ps -> (ch -> th))
4	3	a1i 8	. 2 |- (ps -> (ps -> (ch -> th)))
5	1, 1, 2, 4	e111 16564	1 |- . ph   ⊢   th .

Syntax hints:   -> wi 3   . vd1 16479

This theorem is referenced by:  e11an 16579  e01 16581  e10 16585  elex2VD 16662  elex22VD 16663  eqsbc3rVD 16664  tpid3gVD 16666  3ornot23VD 16671  orbi1rVD 16672  3orbi123VD 16674  sbc3orgVD 16675  sbcoreleleqVD 16683  ordelordaxrVD 16691  sbcim2gVD 16699  trsbcVD 16701  undif3VD 16706

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