Definition df-t 41

Description: Define true.

Assertion

Ref	Expression
df-t	1 = (a v a')

Detailed syntax breakdown of Definition df-t

Step	Hyp	Ref	Expression
1		wt 8	. 2 term 1
2		wva	. . 3 term a
3	2	wn 4	. . 3 term a'
4	2, 3	wo 6	. 2 term (a v a')
5	1, 4	wb 1	1 wff 1 = (a v a')

This definition is referenced by:  dff2 94  or1 98  biid 110  omlem2 122  comm1 173  ka4lemo 222  sklem 224  ska3 226  wlem1 237  lei3 240  mccune2 241  i3id 245  i1id 269  i2id 270  bina5 280  wql2lem5 286  womle2a 289  nom23 310  wdf-c1 369  wlem14 416  ska2 418  ska4 419  woml6 422  woml7 423  r3a 426  r3b 428  oml6 474  comcmtr1 480  i31 506  i3abs3 510  i3th1 529  i3con 537  ud1lem1 546  ud1lem2 547  ud1lem3 548  ud2lem3 551  ud3lem1c 554  ud3lem1 556  ud3lem3 562  ud4lem1c 565  ud4lem1 567  ud4lem2 568  ud4lem3b 570  ud4lem3 571  ud5lem1 575  ud5lem3 580  u1lemoa 606  u2lemoa 607  u4lemoa 609  u4lemona 614  u3lemob 618  u4lemob 619  u1lemonb 621  u2lemonb 622  u3lemonb 623  u1lemc4 687  u2lemc4 688  u3lemc4 689  u4lemc4 690  u5lemc4 691  u1lem3var1 717  u1lem2 730  u2lem2 731  u2lem3 736  u1lem4 743  u4lem4 745  u4lem5 750  u5lem5 751  u4lem6 754  u5lem6 755  u1lem7 758  u1lem11 766  u3lem8 769  u3lem10 771  u3lem11 772  u3lem13a 775  u3lem13b 776  i2i1i1 786  i1abs 787  test 788  test2 789  3vded11 800  3vded12 801  2oalem1 811  neg3antlem2 851  elimconslem 853  elimcons 854  mhlem1 863  gomaex3lem1 900  gomaex3lem2 901  gomaex3lem3 902  gomaex3lem7 906  oa3to4lem1 931  oa3to4lem2 932  oa4to6lem1 946  oa4to6lem2 947  oa4to6lem3 948  lem3.3.7i0e1 1042  lem3.3.7i1e1 1045  lem3.3.7i1e2 1046  lem3.3.7i2e1 1048  lem3.3.7i2e2 1049  lem3.3.7i3e1 1051  lem3.3.7i3e2 1052

Copyright terms: Public domain