Definition df-i1 44

Description: Define Sasaki (Mittelstaedt) conditional.

Assertion

Ref	Expression
df-i1	(a ->1 b) = (a' v (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' v (a ^ b))
7	3, 6	wb 1	1 wff (a ->1 b) = (a' v (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 1036  lem3.3.3lem1 1048  lem3.3.3lem2 1049  lem3.3.5 1054  lem3.3.7i1e1 1059  lem3.4.3 1075  lem4.6.2e1 1079  lem4.6.6i0j1 1085  lem4.6.6i1j0 1089  lem4.6.6i1j3 1091  lem4.6.6i2j1 1093  lem4.6.6i3j1 1096  lem4.6.7 1100  wdwom 1103

Copyright terms: Public domain