Theorem itopi 41

Description: Insert Top into With. Inverse of etopi 42.

Hypothesis

Ref	Expression
itopi.1	⊦ 𝜑

Assertion

Ref	Expression
itopi	⊦ (𝜑 & ⊤)

Proof of Theorem itopi

Step	Hyp	Ref	Expression
1		itopi.1	. 2 ⊦ 𝜑
2		ax-init 7	. . 3 ⊦ (~ 𝜑 ⅋ 𝜑)
3		ax-top 31	. . 3 ⊦ (~ 𝜑 ⅋ ⊤)
4	2, 3	ax-iac 32	. 2 ⊦ (~ 𝜑 ⅋ (𝜑 & ⊤))
5	1, 4	cut1 10	1 ⊦ (𝜑 & ⊤)

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-top 31  ax-iac 32

This theorem is referenced by: (None)