Definition df-i5 48

Description: Define relevance conditional.

Assertion

Ref	Expression
df-i5	(a ->5 b) = (((a ^ b) v (a' ^ b)) v (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) v (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) v (a' ^ b)) v (a' ^ b'))
11	3, 10	wb 1	1 wff (a ->5 b) = (((a ^ b) v (a' ^ b)) v (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 1104

Copyright terms: Public domain