Definition df-i3 45

Description: Define Kalmbach conditional.

Assertion

Ref	Expression
df-i3	(a →3 b) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b)))

Detailed syntax breakdown of Definition df-i3

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

This definition is referenced by:  ska15 236  lei3 238  mccune3 240  i3n1 241  ni31 242  i3id 243  li3 244  ri3 245  i3i4 262  nom13 302  i5lei3 341  i3bi 478  df2i3 480  dfi3b 481  i3lem4 489  comi31 490  com2i3 491  lem4 493  i3abs1 504  i3abs3 506  i3th5 529  i3orlem1 534  i3orlem4 537  ud3lem1a 548  ud3lem1c 550  ud3lem1d 551  ud3lem1 552  ud3lem2 553  ud3lem3d 557  ud3lem3 558  u3lemaa 584  u3lemana 589  u3lemab 594  u3lemanb 599  u3lemoa 604  u3lemona 609  u3lemob 614  u3lemonb 619  u3lemc4 685  u3lem3 733  u3lem7 756  u3lem10 767  u3lem11 768  u3lem13a 771  u3lem13b 772  u3lem14a 773  negantlem9 841  neg3antlem2 847

metamath.org