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