Definition df-i3 46

Description: Define Kalmbach conditional.

Assertion

Ref	Expression
df-i3	(a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v 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) v (a' ^ b'))
9	4, 2	wo 6	. . . 4 term (a' v b)
10	1, 9	wa 7	. . 3 term (a ^ (a' v b))
11	8, 10	wo 6	. 2 term (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))
12	3, 11	wb 1	1 wff (a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))

This definition is referenced by:  ska15 238  lei3 240  mccune3 242  i3n1 243  ni31 244  i3id 245  li3 246  ri3 247  i3i4 264  nom13 304  i5lei3 343  i3bi 482  df2i3 484  dfi3b 485  i3lem4 493  comi31 494  com2i3 495  lem4 497  i3abs1 508  i3abs3 510  i3th5 533  i3orlem1 538  i3orlem4 541  ud3lem1a 552  ud3lem1c 554  ud3lem1d 555  ud3lem1 556  ud3lem2 557  ud3lem3d 561  ud3lem3 562  u3lemaa 588  u3lemana 593  u3lemab 598  u3lemanb 603  u3lemoa 608  u3lemona 613  u3lemob 618  u3lemonb 623  u3lemc4 689  u3lem3 737  u3lem7 760  u3lem10 771  u3lem11 772  u3lem13a 775  u3lem13b 776  u3lem14a 777  negantlem9 845  neg3antlem2 851  lem3.3.7i3e1 1051  lem4.6.6i0j3 1073  lem4.6.6i1j3 1077  lem4.6.6i3j0 1081  lem4.6.6i3j1 1082

Copyright terms: Public domain