Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Virtual Deduction Theorems
ee120
Metamath Proof Explorer
Description: Virtual deduction rule e120 without virtual deduction symbols.
(Contributed by Alan Sare , 14-Jul-2011)
(Proof modification is discouraged.) (New usage is discouraged.)
Ref
Expression
Hypotheses
ee120.1
⊢ ( 𝜑 → 𝜓 )
ee120.2
⊢ ( 𝜑 → ( 𝜒 → 𝜃 ) )
ee120.3
⊢ 𝜏
ee120.4
⊢ ( 𝜓 → ( 𝜃 → ( 𝜏 → 𝜂 ) ) )
Assertion
ee120
⊢ ( 𝜑 → ( 𝜒 → 𝜂 ) )
Proof
Step
Hyp
Ref
Expression
1
ee120.1
⊢ ( 𝜑 → 𝜓 )
2
ee120.2
⊢ ( 𝜑 → ( 𝜒 → 𝜃 ) )
3
ee120.3
⊢ 𝜏
4
ee120.4
⊢ ( 𝜓 → ( 𝜃 → ( 𝜏 → 𝜂 ) ) )
5
1
a1d
⊢ ( 𝜑 → ( 𝜒 → 𝜓 ) )
6
3
a1i
⊢ ( 𝜒 → 𝜏 )
7
6
a1i
⊢ ( 𝜑 → ( 𝜒 → 𝜏 ) )
8
5 2 7 4
ee222
⊢ ( 𝜑 → ( 𝜒 → 𝜂 ) )