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