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 237  ud1lem0a 249  ud1lem0b 250  i1i2 260  0i1 267  1i1 268  i1id 269  ud1lem0c 271  wql1lem 281  wql2lem4 285  oaidlem1 288  womle2a 289  nom10 301  nom11 302  nom12 303  nom13 304  nom14 305  nom15 306  nom20 307  nom21 308  nom22 309  nom23 310  nom24 311  nom25 312  go1 337  i1or 339  i5lei1 341  2vwomr1a 349  2vwomr2a 350  wr5-2v 352  woml6 422  ud1lem1 546  ud1lem2 547  ud1lem3 548  u1lemaa 586  u1lemana 591  u1lemab 596  u1lemanb 601  u1lemoa 606  u1lemona 611  u1lemob 616  u1lemonb 621  u1lemc1 666  u1lemc2 672  u1lemc4 687  u1lemc6 692  comi12 693  comi1 695  u1lemle2 701  u1lembi 706  u12lembi 712  u21lembi 713  u1lemn1b 716  u1lem2 730  u1lem3 735  u1lem4 743  u1lem5 747  u12lem 757  u1lem7 758  u1lem8 762  u1lem9a 763  u1lem9b 764  u1lem11 766  u3lem13a 775  u3lem13b 776  bi1o1a 784  i2i1i1 786  3vth9 798  3vded11 800  3vded12 801  1oa 806  mlalem 818  sa5 822  salem1 823  sadm3 824  bi3 825  bi4 826  imp3 827  orbi 828  i1orni1 833  negantlem1 834  negantlem2 835  negantlem3 836  negantlem4 837  negantlem9 845  negantlem10 847  neg3antlem2 851  neg3ant1 852  elimconslem 853  elimcons 854  elimcons2 855  comanblem1 856  comanb 858  mlaconjolem 871  cancellem 877  gomaex3h7 894  gomaex3h10 897  gomaex3lem3 902  gomaex3lem4 903  gomaex3 910  oas 911  oat 913  oatr 914  oaidlem2 917  oaidlem2g 918  oa3to4lem1 931  oa3to4lem2 932  oa6to4h1 941  oa6to4h2 942  oa6to4h3 943  oa4to6lem1 946  oa4to6lem2 947  oa4to6lem3 948  oa4btoc 952  oa3-2lemb 965  oa3-6lem 966  oa3-3lem 967  oa3-4lem 969  oa3-5lem 970  oa3-u1lem 971  oa3-u2lem 972  oa3-2to2s 976  d3oa 981  axoa4a 1022  lem3.3.3lem1 1034  lem3.3.3lem2 1035  lem3.3.5 1040  lem3.3.7i1e1 1045  lem3.4.3 1061  lem4.6.2e1 1065  lem4.6.6i0j1 1071  lem4.6.6i1j0 1075  lem4.6.6i1j3 1077  lem4.6.6i2j1 1079  lem4.6.6i3j1 1082  lem4.6.7 1086  wdwom 1089

Copyright terms: Public domain