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