Metamath Proof Explorer


Theorem e123

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

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

Proof

Step Hyp Ref Expression
1 e123.1 φψ
2 e123.2 φ,χθ
3 e123.3 φ,χ,τη
4 e123.4 ψθηζ
5 1 vd13 φ,χ,τψ
6 2 vd23 φ,χ,τθ
7 5 6 3 4 e333 φ,χ,τζ