Theorem e00 16635

Description: Elimination rule identical to mp2 54. The non-virtual deduction form is the virtual deduction form, which is mp2 54.

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 54	1 |- ch

Syntax hints:   -> wi 3

This theorem is referenced by:  3impexpVD 16680  3impexpbicomVD 16681  hbra2VD 16684

This theorem was proved from axioms:  ax-mp 7

Copyright terms: Public domain