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