Metamath Proof Explorer


Theorem e020

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

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

Proof

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