Theorem e00 38995

Description: Elimination rule identical to mp2 9. The non-virtual deduction form is the virtual deduction form, which is mp2 9. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e00.1	|- ph
e00.2	|- ps
e00.3	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
e00	|- ch

Proof of Theorem e00

Step	Hyp	Ref	Expression
1		e00.1	. 2 |- ph
2		e00.2	. 2 |- ps
3		e00.3	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 2, 3	mp2 9	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  3impexpVD  39091  3impexpbicomVD  39092  onfrALTlem5VD  39121