Definition df-i4 47

Description: Define non-tollens conditional. (Contributed by NM, 23-Nov-1997.)

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 15	. 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  262  ud4lem0b  263  i3i4  270  ud4lem0c  280  nom14  311  i5lei4  350  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1  581  ud4lem2  582  ud4lem3  585  u4lemaa  603  u4lemana  608  u4lemab  613  u4lemanb  618  u4lemoa  623  u4lemona  628  u4lemob  633  u4lemonb  638  u4lemc1  683  u4lemc2  689  u4lemc4  704  u4lemle2  718  u4lem1  737  u4lem4  759  u4lem5  764  u4lem6  768  negantlem10  861  lem3.3.7i4e1  1069  lem4.6.6i0j4  1091  lem4.6.6i2j4  1097  lem4.6.6i4j0  1100  lem4.6.6i4j2  1101