Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Virtual Deduction Theorems
e100
Metamath Proof Explorer
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
⊢ φ → τ