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 258  ud5lem0b 259  i5con 266  ud5lem0c 275  nom15 306  i5lei1 341  i5lei2 342  i5lei3 343  i5lei4 344  ud5lem1a 572  ud5lem1b 573  ud5lem1 575  ud5lem2 576  ud5lem3a 577  ud5lem3 580  u5lemaa 590  u5lemana 595  u5lemab 600  u5lemanb 605  u5lemoa 610  u5lemona 615  u5lemob 620  u5lemonb 625  u5lemc1 670  u5lemc1b 671  u5lemc2 676  u5lemc4 691  u5lemle2 705  u5lembi 711  u5lem5 751  u5lem6 755  u24lem 756  lem3.3.7i5e1 1057  wdwom 1089

Copyright terms: Public domain