Definition df-i2 45

Description: Define Dishkant conditional.

Assertion

Ref	Expression
df-i2	(a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))

Detailed syntax breakdown of Definition df-i2

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wi2 13	. 2 term  (a →2 b)
4	1	wn 4	. . . 4 term  a⊥
5	2	wn 4	. . . 4 term  b⊥
6	4, 5	wa 7	. . 3 term  (a⊥ ∩ b⊥ )
7	2, 6	wo 6	. 2 term  (b ∪ (a⊥ ∩ b⊥ ))
8	3, 7	wb 1	1 wff  (a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))

This definition is referenced by:  ud2lem0a 258  ud2lem0b 259  i1i2 266  i2id 276  ud2lem0c 278  wql2lem 288  wql2lem2 289  wql2lem3 290  wql2lem5 292  wql1 293  nom12 309  i2or 344  lei2 346  i5lei2 348  2vwomr1a 363  2vwomr2a 364  2vwomlem 365  wr5-2v 366  woml6 436  woml7 437  ud2lem1 563  ud2lem2 564  ud2lem3 565  u2lemaa 601  u2lemana 606  u2lemab 611  u2lemanb 616  u2lemoa 621  u2lemona 626  u2lemob 631  u2lemonb 636  u2lemc1 681  u2lemc2 687  u2lemc4 702  comi12 707  u2lemle2 716  u2lembi 721  i2bi 722  u12lembi 726  u2lem1 735  u2lem2 745  u2lem3 750  u2lem5 762  u24lem 770  u12lem 771  u2lem7 773  u2lem8 782  i2i1i1 800  3vth1 804  3vth4 807  3vth5 808  3vth6 809  3vth7 810  3vth9 812  3vded21 817  3vded22 818  1oa 820  1oaii 824  2oalem1 825  2oath1 826  oale 829  3vroa 831  salem1 837  bi3 839  orbi 842  negant2 858  mlaconjolem 885  govar 896  govar2 897  oa4lem1 937  oa4lem2 938  distoah4 943  d3oa 995  oalii 1002  oaliv 1003  oalem1 1005  oadist2a 1007  mloa 1018  lem3.3.4 1052  lem3.3.6 1055  lem3.3.7i2e1 1062  lem4.6.6i0j2 1086  lem4.6.6i2j0 1092  lem4.6.6i2j1 1093  lem4.6.6i2j4 1094  lem4.6.6i4j2 1098  wdwom 1103

Copyright terms: Public domain