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 100  or1 104  biid 116  omlem2 128  comm1 179  ka4lemo 228  sklem 230  ska3 232  wlem1 243  lei3 246  mccune2 247  i3id 251  i1id 275  i2id 276  bina5 286  wql2lem5 292  womle2a 295  nom23 316  wdf-c1 383  wlem14 430  ska2 432  ska4 433  woml6 436  woml7 437  r3a 440  r3b 442  oml6 488  comcmtr1 494  i31 520  i3abs3 524  i3th1 543  i3con 551  ud1lem1 560  ud1lem2 561  ud1lem3 562  ud2lem3 565  ud3lem1c 568  ud3lem1 570  ud3lem3 576  ud4lem1c 579  ud4lem1 581  ud4lem2 582  ud4lem3b 584  ud4lem3 585  ud5lem1 589  ud5lem3 594  u1lemoa 620  u2lemoa 621  u4lemoa 623  u4lemona 628  u3lemob 632  u4lemob 633  u1lemonb 635  u2lemonb 636  u3lemonb 637  u1lemc4 701  u2lemc4 702  u3lemc4 703  u4lemc4 704  u5lemc4 705  u1lem3var1 731  u1lem2 744  u2lem2 745  u2lem3 750  u1lem4 757  u4lem4 759  u4lem5 764  u5lem5 765  u4lem6 768  u5lem6 769  u1lem7 772  u1lem11 780  u3lem8 783  u3lem10 785  u3lem11 786  u3lem13a 789  u3lem13b 790  i2i1i1 800  i1abs 801  test 802  test2 803  3vded11 814  3vded12 815  2oalem1 825  neg3antlem2 865  elimconslem 867  elimcons 868  mhlem1 877  gomaex3lem1 914  gomaex3lem2 915  gomaex3lem3 916  gomaex3lem7 920  oa3to4lem1 945  oa3to4lem2 946  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  lem3.3.7i0e1 1056  lem3.3.7i1e1 1059  lem3.3.7i1e2 1060  lem3.3.7i2e1 1062  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066

Copyright terms: Public domain