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
⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) → 𝜂 )