Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Virtual Deduction Theorems
el0321old
Metamath Proof Explorer
Description: A virtual deduction elimination rule. (Contributed by Alan Sare , 13-Jun-2015) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypotheses
el0321old.1
⊢ 𝜑
el0321old.2
⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜏 )
el0321old.3
⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜂 )
Assertion
el0321old
⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜂 )
Proof
Step
Hyp
Ref
Expression
1
el0321old.1
⊢ 𝜑
2
el0321old.2
⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜏 )
3
el0321old.3
⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜂 )
4
2
dfvd3ani
⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) → 𝜏 )
5
1 4 3
eel0321old
⊢ ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) → 𝜂 )
6
5
dfvd3anir
⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜂 )