Definition df-i4 47

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 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 1068  lem4.6.6i0j4 1088  lem4.6.6i2j4 1094  lem4.6.6i4j0 1097  lem4.6.6i4j2 1098

Copyright terms: Public domain