Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Virtual Deduction Theorems
e1111
Metamath Proof Explorer
Description: A virtual deduction elimination rule. (Contributed by Alan Sare , 6-Mar-2012) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypotheses
e1111.1
⊢ ( 𝜑 ▶ 𝜓 )
e1111.2
⊢ ( 𝜑 ▶ 𝜒 )
e1111.3
⊢ ( 𝜑 ▶ 𝜃 )
e1111.4
⊢ ( 𝜑 ▶ 𝜏 )
e1111.5
⊢ ( 𝜓 → ( 𝜒 → ( 𝜃 → ( 𝜏 → 𝜂 ) ) ) )
Assertion
e1111
⊢ ( 𝜑 ▶ 𝜂 )
Proof
Step
Hyp
Ref
Expression
1
e1111.1
⊢ ( 𝜑 ▶ 𝜓 )
2
e1111.2
⊢ ( 𝜑 ▶ 𝜒 )
3
e1111.3
⊢ ( 𝜑 ▶ 𝜃 )
4
e1111.4
⊢ ( 𝜑 ▶ 𝜏 )
5
e1111.5
⊢ ( 𝜓 → ( 𝜒 → ( 𝜃 → ( 𝜏 → 𝜂 ) ) ) )
6
1
in1
⊢ ( 𝜑 → 𝜓 )
7
2
in1
⊢ ( 𝜑 → 𝜒 )
8
3
in1
⊢ ( 𝜑 → 𝜃 )
9
4
in1
⊢ ( 𝜑 → 𝜏 )
10
6 7 8 9 5
ee1111
⊢ ( 𝜑 → 𝜂 )
11
10
dfvd1ir
⊢ ( 𝜑 ▶ 𝜂 )