Metamath Proof Explorer


Theorem eel0321old

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 ⊢ ψ ∧ χ ∧ θ → η