Definition df-i3 46

Description: Define Kalmbach conditional. (Contributed by NM, 2-Nov-1997.)

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 14	. 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  244  lei3  246  mccune3  248  i3n1  249  ni31  250  i3id  251  li3  252  ri3  253  i3i4  270  nom13  310  i5lei3  349  i3bi  496  df2i3  498  dfi3b  499  i3lem4  507  comi31  508  com2i3  509  lem4  511  i3abs1  522  i3abs3  524  i3th5  547  i3orlem1  552  i3orlem4  555  ud3lem1a  566  ud3lem1c  568  ud3lem1d  569  ud3lem1  570  ud3lem2  571  ud3lem3d  575  ud3lem3  576  u3lemaa  602  u3lemana  607  u3lemab  612  u3lemanb  617  u3lemoa  622  u3lemona  627  u3lemob  632  u3lemonb  637  u3lemc4  703  u3lem3  751  u3lem7  774  u3lem10  785  u3lem11  786  u3lem13a  789  u3lem13b  790  u3lem14a  791  negantlem9  859  neg3antlem2  865  lem3.3.7i3e1  1066  lem4.6.6i0j3  1090  lem4.6.6i1j3  1094  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099