Definition df-lb 56

Description: Definition of linear biconditional. Since the linear implication has not been defined, this is a mouthfull. The good news is, once the properties of the linear biconditional are proven, it will be much easier to express other definitions. See dflb 93 for a cleaner form of the definition.

Assertion

Ref	Expression
df-lb	⊦ ((~ (𝜑 ⧟ 𝜓) ⅋ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑))) & (~ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)) ⅋ (𝜑 ⧟ 𝜓)))

Detailed syntax breakdown of Definition df-lb

Step	Hyp	Ref	Expression
1		wph	. . . . 5 wff 𝜑
2		wps	. . . . 5 wff 𝜓
3	1, 2	wlb 55	. . . 4 wff (𝜑 ⧟ 𝜓)
4	3	wneg 3	. . 3 wff ~ (𝜑 ⧟ 𝜓)
5	1	wneg 3	. . . . 5 wff ~ 𝜑
6	5, 2	wmd 2	. . . 4 wff (~ 𝜑 ⅋ 𝜓)
7	2	wneg 3	. . . . 5 wff ~ 𝜓
8	7, 1	wmd 2	. . . 4 wff (~ 𝜓 ⅋ 𝜑)
9	6, 8	wac 30	. . 3 wff ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑))
10	4, 9	wmd 2	. 2 wff (~ (𝜑 ⧟ 𝜓) ⅋ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)))
11	9	wneg 3	. . 3 wff ~ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑))
12	11, 3	wmd 2	. 2 wff (~ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)) ⅋ (𝜑 ⧟ 𝜓))
13	10, 12	wac 30	1 wff ((~ (𝜑 ⧟ 𝜓) ⅋ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑))) & (~ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)) ⅋ (𝜑 ⧟ 𝜓)))

This definition is referenced by:  lb1d  57  lb2d  58  lbi1s  87  lbi2s  88  dflb2s  92