Definition df-i4 47

Description: Define non-tollens conditional.

Assertion

Ref	Expression
df-i4	(a ->4 b) = (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))

Detailed syntax breakdown of Definition df-i4

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . 3 term b
3	1, 2	wi4 15	. 2 term (a ->4 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	5, 2	wo 6	. . . 4 term (a' v b)
9	2	wn 4	. . . 4 term b'
10	8, 9	wa 7	. . 3 term ((a' v b) ^ b')
11	7, 10	wo 6	. 2 term (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))
12	3, 11	wb 1	1 wff (a ->4 b) = (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))

This definition is referenced by:  ud4lem0a 256  ud4lem0b 257  i3i4 264  ud4lem0c 274  nom14 305  i5lei4 344  ud4lem1a 563  ud4lem1b 564  ud4lem1c 565  ud4lem1 567  ud4lem2 568  ud4lem3 571  u4lemaa 589  u4lemana 594  u4lemab 599  u4lemanb 604  u4lemoa 609  u4lemona 614  u4lemob 619  u4lemonb 624  u4lemc1 669  u4lemc2 675  u4lemc4 690  u4lemle2 704  u4lem1 723  u4lem4 745  u4lem5 750  u4lem6 754  negantlem10 847  lem3.3.7i4e1 1054  lem4.6.6i0j4 1074  lem4.6.6i2j4 1080  lem4.6.6i4j0 1083  lem4.6.6i4j2 1084

Copyright terms: Public domain