Definition df-i2 45

Description: Define Dishkant conditional. (Contributed by NM, 23-Nov-1997.)

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  1053  lem3.3.6  1056  lem3.3.7i2e1  1063  lem4.6.6i0j2  1089  lem4.6.6i2j0  1095  lem4.6.6i2j1  1096  lem4.6.6i2j4  1097  lem4.6.6i4j2  1101  wdwom  1106