ax-ebot - Linear Logic Proof Explorer

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

Axiom ax-ebot 5

Description: Remove a ⊥. Inverse of ax-ibot 4.

**Hypothesis**
Ref	Expression
ax-ebot.1	⊦ (⊥ ⅋ 𝜑)

**Assertion**
Ref	Expression
ax-ebot	⊦ 𝜑

**Detailed syntax breakdown of Axiom ax-ebot**
Step	Hyp	Ref	Expression
1		wph	1 wff 𝜑

Colors of variables: wff var nilad

This axiom is referenced by: cut1 10 mdasri 17 ebotr 19 enenebot 28 iaci 36 lb1i 59 lb2i 60 dfli1i 65 dfli2i 66 mdm1i 71 mdm2i 72 lmp 76 acm1i 82 acm2i 83