Definition df-i5 48

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

Assertion

Ref	Expression
df-i5	(a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))

Detailed syntax breakdown of Definition df-i5

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wi5 16	. 2 term  (a →5 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	2	wn 4	. . . 4 term  b⊥
9	5, 8	wa 7	. . 3 term  (a⊥ ∩ b⊥ )
10	7, 9	wo 6	. 2 term  (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
11	3, 10	wb 1	1 wff  (a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))

This definition is referenced by:  ud5lem0a  264  ud5lem0b  265  i5con  272  ud5lem0c  281  nom15  312  i5lei1  347  i5lei2  348  i5lei3  349  i5lei4  350  ud5lem1a  586  ud5lem1b  587  ud5lem1  589  ud5lem2  590  ud5lem3a  591  ud5lem3  594  u5lemaa  604  u5lemana  609  u5lemab  614  u5lemanb  619  u5lemoa  624  u5lemona  629  u5lemob  634  u5lemonb  639  u5lemc1  684  u5lemc1b  685  u5lemc2  690  u5lemc4  705  u5lemle2  719  u5lembi  725  u5lem5  765  u5lem6  769  u24lem  770  lem3.3.7i5e1  1072  wdwom  1106