Axiom ax-ibot 4

Description: Add a ⊥. Inverse of ax-ebot 5.

Hypothesis

Ref	Expression
ax-ibot.1	⊦ 𝜑

Assertion

Ref	Expression
ax-ibot	⊦ (⊥ ⅋ 𝜑)

Detailed syntax breakdown of Axiom ax-ibot

Step	Hyp	Ref	Expression
1		wbot 1	. 2 wff ⊥
2		wph	. 2 wff 𝜑
3	1, 2	wmd 2	1 wff (⊥ ⅋ 𝜑)

This axiom is referenced by:  cut1  10  mdasri  17  ibotr  18  inenebot  27  iaci  36  lb1i  59  lb2i  60  dfli1i  65  dfli2i  66  mdm1i  71  mdm2i  72  lmp  76  acm1i  82  acm2i  83  md1  113