etopi - Linear Logic Proof Explorer

	Linear Logic Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > LLPE Home > Th. List > etopi		Structured version

Theorem etopi 42

Description: Remove Top from With. This is, of course, just a special case of ax-eac1 33.

**Hypothesis**
Ref	Expression
etopi.1	⊦ (𝜑 & ⊤)

**Assertion**
Ref	Expression
etopi	⊦ 𝜑

**Proof of Theorem etopi**
Step	Hyp	Ref	Expression
1		etopi.1	. 2 ⊦ (𝜑 & ⊤)
2	1	eac1i 38	1 ⊦ 𝜑

Colors of variables: wff var nilad

Syntax hints: ⊤wtop 29 & wac 30

This theorem was proved from axioms: ax-ibot 4 ax-ebot 5 ax-cut 6 ax-init 7 ax-mdco 8 ax-eac1 33

This theorem is referenced by: (None)