Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Virtual Deduction Theorems
e020
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
e020.1
⊢ φ
e020.2
⊢ ψ , χ → θ
e020.3
⊢ τ
e020.4
⊢ φ → θ → τ → η
Assertion
e020
⊢ ψ , χ → η
Proof
Step
Hyp
Ref
Expression
1
e020.1
⊢ φ
2
e020.2
⊢ ψ , χ → θ
3
e020.3
⊢ τ
4
e020.4
⊢ φ → θ → τ → η
5
1
vd02
⊢ ψ , χ → φ
6
3
vd02
⊢ ψ , χ → τ
7
5 2 6 4
e222
⊢ ψ , χ → η