Metamath Proof Explorer


Theorem e200

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

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

Proof

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