Metamath Proof Explorer


Theorem e100

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

Ref Expression
Hypotheses e100.1 φ ψ
e100.2 χ
e100.3 θ
e100.4 ψ χ θ τ
Assertion e100 φ τ

Proof

Step Hyp Ref Expression
1 e100.1 φ ψ
2 e100.2 χ
3 e100.3 θ
4 e100.4 ψ χ θ τ
5 2 vd01 φ χ
6 3 vd01 φ θ
7 1 5 6 4 e111 φ τ