Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Virtual Deduction Theorems
eel0321old
Metamath Proof Explorer
Description: el0321old without virtual deductions. (Contributed by Alan Sare , 13-Jun-2015) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypotheses
eel0321old.1
⊢ φ
eel0321old.2
⊢ ψ ∧ χ ∧ θ → τ
eel0321old.3
⊢ φ ∧ τ → η
Assertion
eel0321old
⊢ ψ ∧ χ ∧ θ → η
Proof
Step
Hyp
Ref
Expression
1
eel0321old.1
⊢ φ
2
eel0321old.2
⊢ ψ ∧ χ ∧ θ → τ
3
eel0321old.3
⊢ φ ∧ τ → η
4
1 2 3
sylancr
⊢ ψ ∧ χ ∧ θ → η