Metamath Proof Explorer


Theorem e002

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses e002.1 φ
e002.2 ψ
e002.3 χ , θ τ
e002.4 φ ψ τ η
Assertion e002 χ , θ η

Proof

Step Hyp Ref Expression
1 e002.1 φ
2 e002.2 ψ
3 e002.3 χ , θ τ
4 e002.4 φ ψ τ η
5 1 vd02 χ , θ φ
6 2 vd02 χ , θ ψ
7 5 6 3 4 e222 χ , θ η