Metamath Proof Explorer


Theorem e120

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

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

Proof

Step Hyp Ref Expression
1 e120.1 φ ψ
2 e120.2 φ , χ θ
3 e120.3 τ
4 e120.4 ψ θ τ η
5 1 vd12 φ , χ ψ
6 5 2 3 4 e220 φ , χ η