Definition df-im 181

Description: Definition of →. It's ⊸ but with some ! splashed in for good measure. Note that only 𝜑 needs the exponential. When this statement is beneath a ! or at the top level, this is equivalent to both sides having the exponential, because of

Assertion

Ref	Expression
df-im	⊦ ((𝜑 → 𝜓) ⧟ (! 𝜑 ⊸ 𝜓))

Detailed syntax breakdown of Definition df-im

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wim 180	. 2 wff (𝜑 → 𝜓)
4	1	wpe 148	. . 3 wff ! 𝜑
5	4, 2	wli 61	. 2 wff (! 𝜑 ⊸ 𝜓)
6	3, 5	wlb 55	1 wff ((𝜑 → 𝜓) ⧟ (! 𝜑 ⊸ 𝜓))

This definition is referenced by: (None)