Theorem nic-id

Description: Theorem id expressed with -/\ . (Contributed by Jeff Hoffman, 17-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nic-id	⊢ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) )

Proof

Step	Hyp	Ref	Expression
1		nic-ax	⊢ ( ( 𝜓 ⊼ ( 𝜓 ⊼ 𝜓 ) ) ⊼ ( ( 𝜃 ⊼ ( 𝜃 ⊼ 𝜃 ) ) ⊼ ( ( 𝜑 ⊼ 𝜓 ) ⊼ ( ( 𝜓 ⊼ 𝜑 ) ⊼ ( 𝜓 ⊼ 𝜑 ) ) ) ) )
2	1	nic-idlem2	⊢ ( ( ( ( 𝜑 ⊼ 𝜓 ) ⊼ ( ( 𝜓 ⊼ 𝜑 ) ⊼ ( 𝜓 ⊼ 𝜑 ) ) ) ⊼ ( 𝜒 ⊼ ( 𝜒 ⊼ 𝜒 ) ) ) ⊼ ( 𝜓 ⊼ ( 𝜓 ⊼ 𝜓 ) ) )
3		nic-idlem1	⊢ ( ( ( 𝜒 ⊼ ( 𝜒 ⊼ 𝜒 ) ) ⊼ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ) ⊼ ( ( ( ( 𝜑 ⊼ 𝜓 ) ⊼ ( ( 𝜓 ⊼ 𝜑 ) ⊼ ( 𝜓 ⊼ 𝜑 ) ) ) ⊼ ( 𝜒 ⊼ ( 𝜒 ⊼ 𝜒 ) ) ) ⊼ ( ( ( 𝜑 ⊼ 𝜓 ) ⊼ ( ( 𝜓 ⊼ 𝜑 ) ⊼ ( 𝜓 ⊼ 𝜑 ) ) ) ⊼ ( 𝜒 ⊼ ( 𝜒 ⊼ 𝜒 ) ) ) ) )
4	3	nic-idlem2	⊢ ( ( ( ( ( 𝜑 ⊼ 𝜓 ) ⊼ ( ( 𝜓 ⊼ 𝜑 ) ⊼ ( 𝜓 ⊼ 𝜑 ) ) ) ⊼ ( 𝜒 ⊼ ( 𝜒 ⊼ 𝜒 ) ) ) ⊼ ( 𝜓 ⊼ ( 𝜓 ⊼ 𝜓 ) ) ) ⊼ ( ( 𝜒 ⊼ ( 𝜒 ⊼ 𝜒 ) ) ⊼ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ) )
5	2 4	nic-mp	⊢ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) )