Definition df-i4 46

Description: Define non-tollens conditional.

Assertion

Ref	Expression
df-i4	(a →4 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ ))

Detailed syntax breakdown of Definition df-i4

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wi4 16	. 2 term  (a →4 b)
4	1, 2	wa 7	. . . 4 term  (a ∩ b)
5	1	wn 4	. . . . 5 term  a⊥
6	5, 2	wa 7	. . . 4 term  (a⊥ ∩ b)
7	4, 6	wo 6	. . 3 term  ((a ∩ b) ∪ (a⊥ ∩ b))
8	5, 2	wo 6	. . . 4 term  (a⊥ ∪ b)
9	2	wn 4	. . . 4 term  b⊥
10	8, 9	wa 7	. . 3 term  ((a⊥ ∪ b) ∩ b⊥ )
11	7, 10	wo 6	. 2 term  (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ ))
12	3, 11	wb 1	1 wff  (a →4 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ ))

This definition is referenced by:  ud4lem0a 254  ud4lem0b 255  i3i4 262  ud4lem0c 272  nom14 303  i5lei4 342  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1 563  ud4lem2 564  ud4lem3 567  u4lemaa 585  u4lemana 590  u4lemab 595  u4lemanb 600  u4lemoa 605  u4lemona 610  u4lemob 615  u4lemonb 620  u4lemc1 665  u4lemc2 671  u4lemc4 686  u4lemle2 700  u4lem1 719  u4lem4 741  u4lem5 746  u4lem6 750  negantlem10 843

metamath.org