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 244  lei3 246  mccune3 248  i3n1 249  ni31 250  i3id 251  li3 252  ri3 253  i3i4 270  nom13 310  i5lei3 349  i3bi 496  df2i3 498  dfi3b 499  i3lem4 507  comi31 508  com2i3 509  lem4 511  i3abs1 522  i3abs3 524  i3th5 547  i3orlem1 552  i3orlem4 555  ud3lem1a 566  ud3lem1c 568  ud3lem1d 569  ud3lem1 570  ud3lem2 571  ud3lem3d 575  ud3lem3 576  u3lemaa 602  u3lemana 607  u3lemab 612  u3lemanb 617  u3lemoa 622  u3lemona 627  u3lemob 632  u3lemonb 637  u3lemc4 703  u3lem3 751  u3lem7 774  u3lem10 785  u3lem11 786  u3lem13a 789  u3lem13b 790  u3lem14a 791  negantlem9 859  neg3antlem2 865  lem3.3.7i3e1 1065  lem4.6.6i0j3 1087  lem4.6.6i1j3 1091  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096

Copyright terms: Public domain