Definition df-t 40

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 9	. 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 92  or1 96  biid 108  omlem2 120  comm1 171  ka4lemo 220  sklem 222  ska3 224  wlem1 235  lei3 238  mccune2 239  i3id 243  i1id 267  i2id 268  bina5 278  wql2lem5 284  womle2a 287  nom23 308  wdf-c1 365  wlem14 412  ska2 414  ska4 415  woml6 418  woml7 419  r3a 422  r3b 424  oml6 470  comcmtr1 476  i31 502  i3abs3 506  i3th1 525  i3con 533  ud1lem1 542  ud1lem2 543  ud1lem3 544  ud2lem3 547  ud3lem1c 550  ud3lem1 552  ud3lem3 558  ud4lem1c 561  ud4lem1 563  ud4lem2 564  ud4lem3b 566  ud4lem3 567  ud5lem1 571  ud5lem3 576  u1lemoa 602  u2lemoa 603  u4lemoa 605  u4lemona 610  u3lemob 614  u4lemob 615  u1lemonb 617  u2lemonb 618  u3lemonb 619  u1lemc4 683  u2lemc4 684  u3lemc4 685  u4lemc4 686  u5lemc4 687  u1lem3var1 713  u1lem2 726  u2lem2 727  u2lem3 732  u1lem4 739  u4lem4 741  u4lem5 746  u5lem5 747  u4lem6 750  u5lem6 751  u1lem7 754  u1lem11 762  u3lem8 765  u3lem10 767  u3lem11 768  u3lem13a 771  u3lem13b 772  i2i1i1 782  i1abs 783  test 784  test2 785  3vded11 796  3vded12 797  2oalem1 807  neg3antlem2 847  elimconslem 849  elimcons 850  mhlem1 859  gomaex3lem1 894  gomaex3lem2 895  gomaex3lem3 896  gomaex3lem7 900  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942

metamath.org