Definition df-t 41

Description: Define true. (Contributed by NM, 9-Aug-1997.)

Assertion

Ref	Expression
df-t	1 = (a ∪ 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 ∪ a⊥ )
5	1, 4	wb 1	1 wff  1 = (a ∪ 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  1057  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067