Definition df-i1 44

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

Assertion

Ref	Expression
df-i1	(a →1 b) = (a⊥ ∪ (a ∩ b))

Detailed syntax breakdown of Definition df-i1

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

This definition is referenced by:  wlem1  243  ud1lem0a  255  ud1lem0b  256  i1i2  266  0i1  273  1i1  274  i1id  275  ud1lem0c  277  wql1lem  287  wql2lem4  291  oaidlem1  294  womle2a  295  nom10  307  nom11  308  nom12  309  nom13  310  nom14  311  nom15  312  nom20  313  nom21  314  nom22  315  nom23  316  nom24  317  nom25  318  go1  343  i1or  345  i5lei1  347  2vwomr1a  363  2vwomr2a  364  wr5-2v  366  woml6  436  ud1lem1  560  ud1lem2  561  ud1lem3  562  u1lemaa  600  u1lemana  605  u1lemab  610  u1lemanb  615  u1lemoa  620  u1lemona  625  u1lemob  630  u1lemonb  635  u1lemc1  680  u1lemc2  686  u1lemc4  701  u1lemc6  706  comi12  707  comi1  709  u1lemle2  715  u1lembi  720  u12lembi  726  u21lembi  727  u1lemn1b  730  u1lem2  744  u1lem3  749  u1lem4  757  u1lem5  761  u12lem  771  u1lem7  772  u1lem8  776  u1lem9a  777  u1lem9b  778  u1lem11  780  u3lem13a  789  u3lem13b  790  bi1o1a  798  i2i1i1  800  3vth9  812  3vded11  814  3vded12  815  1oa  820  mlalem  832  sa5  836  salem1  837  sadm3  838  bi3  839  bi4  840  imp3  841  orbi  842  i1orni1  847  negantlem1  848  negantlem2  849  negantlem3  850  negantlem4  851  negantlem9  859  negantlem10  861  neg3antlem2  865  neg3ant1  866  elimconslem  867  elimcons  868  elimcons2  869  comanblem1  870  comanb  872  mlaconjolem  885  cancellem  891  gomaex3h7  908  gomaex3h10  911  gomaex3lem3  916  gomaex3lem4  917  gomaex3  924  oas  925  oat  927  oatr  928  oaidlem2  931  oaidlem2g  932  oa3to4lem1  945  oa3to4lem2  946  oa6to4h1  955  oa6to4h2  956  oa6to4h3  957  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4btoc  966  oa3-2lemb  979  oa3-6lem  980  oa3-3lem  981  oa3-4lem  983  oa3-5lem  984  oa3-u1lem  985  oa3-u2lem  986  oa3-2to2s  990  d3oa  995  axoa4a  1037  lem3.3.3lem1  1049  lem3.3.3lem2  1050  lem3.3.5  1055  lem3.3.7i1e1  1060  lem3.4.3  1076  thm3.8i1lem  1080  lem4.6.2e1  1082  lem4.6.6i0j1  1088  lem4.6.6i1j0  1092  lem4.6.6i1j3  1094  lem4.6.6i2j1  1096  lem4.6.6i3j1  1099  lem4.6.7  1103  wdwom  1106