Definition df-a 40

Description: Define conjunction.

Assertion

Ref	Expression
df-a	(a ^ b) = (a' v b')'

Detailed syntax breakdown of Definition df-a

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

This definition is referenced by:  ancom 74  anass 76  lan 77  oran 87  anor1 88  anor2 89  oran3 93  dfb 94  dfnb 95  an1 106  an0 108  anidm 111  a5b 120  a5c 121  di 126  wwfh1 216  wwfh2 217  wwfh3 218  wwfh4 219  ka4lem 229  ni31 250  ud1lem0c 277  ud4lem0c 280  ud5lem0c 281  wran 369  wcomlem 382  wcomdr 421  wfh1 423  wfh2 424  wfh3 425  wfh4 426  wcom2an 428  woml6 436  omla 447  comcom 453  comdr 466  df2c1 468  fh1 469  fh2 470  fh3 471  fh4 472  com2an 484  gsth2 490  i3ran 535  i3con 551  ud1lem1 560  ud3lem3 576  ud4lem1b 578  ud4lem1c 579  ud4lem1 581  ud5lem1b 587  ud5lem1 589  ud5lem3 594  u4lemona 628  u1lemonb 635  u1lemnaa 640  u5lemnaa 644  u4lemnab 653  u5lemnab 654  u1lemnona 665  u2lemnona 666  u3lemnona 667  u4lemnona 668  u5lemnona 669  u1lemnonb 675  u2lemnonb 676  u3lemnonb 677  u4lemnonb 678  u5lemnonb 679  u3lem1n 741  u4lem1n 742  u5lem1n 743  u4lem3n 755  u5lem3n 756  u3lem12 788  i1abs 801  test2 803  2oath1 826  elimconslem 867  elimcons 868  mlaconjo 886  oa6todual 952  oa8todual 971  oal1 1000

Copyright terms: Public domain