Definition df-i2 44

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 14	. 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 250  ud2lem0b 251  i1i2 258  i2id 268  ud2lem0c 270  wql2lem 280  wql2lem2 281  wql2lem3 282  wql2lem5 284  wql1 285  nom12 301  i2or 336  lei2 338  i5lei2 340  2vwomr1a 345  2vwomr2a 346  2vwomlem 347  wr5-2v 348  woml6 418  woml7 419  ud2lem1 545  ud2lem2 546  ud2lem3 547  u2lemaa 583  u2lemana 588  u2lemab 593  u2lemanb 598  u2lemoa 603  u2lemona 608  u2lemob 613  u2lemonb 618  u2lemc1 663  u2lemc2 669  u2lemc4 684  comi12 689  u2lemle2 698  u2lembi 703  i2bi 704  u12lembi 708  u2lem1 717  u2lem2 727  u2lem3 732  u2lem5 744  u24lem 752  u12lem 753  u2lem7 755  u2lem8 764  i2i1i1 782  3vth1 786  3vth4 789  3vth5 790  3vth6 791  3vth7 792  3vth9 794  3vded21 799  3vded22 800  1oa 802  1oaii 806  2oalem1 807  2oath1 808  oale 811  3vroa 813  salem1 819  bi3 821  orbi 824  negant2 840  mlaconjolem 867  govar 876  govar2 877  oa4lem1 917  oa4lem2 918  distoah4 923  d3oa 975  oalii 982  oaliv 983  oalem1 985  oadist2a 987  mloa 998

metamath.org