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