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 69  anass 70  lan 71  oran 81  anor1 82  anor2 83  oran3 87  dfb 88  dfnb 89  an1 100  an0 102  anidm 105  a5b 114  a5c 115  di 120  wwfh1 210  wwfh2 211  wwfh3 212  wwfh4 213  ka4lem 223  ni31 244  ud1lem0c 271  ud4lem0c 274  ud5lem0c 275  wran 355  wcomlem 368  wcomdr 407  wfh1 409  wfh2 410  wfh3 411  wfh4 412  wcom2an 414  woml6 422  omla 433  comcom 439  comdr 452  df2c1 454  fh1 455  fh2 456  fh3 457  fh4 458  com2an 470  gsth2 476  i3ran 521  i3con 537  ud1lem1 546  ud3lem3 562  ud4lem1b 564  ud4lem1c 565  ud4lem1 567  ud5lem1b 573  ud5lem1 575  ud5lem3 580  u4lemona 614  u1lemonb 621  u1lemnaa 626  u5lemnaa 630  u4lemnab 639  u5lemnab 640  u1lemnona 651  u2lemnona 652  u3lemnona 653  u4lemnona 654  u5lemnona 655  u1lemnonb 661  u2lemnonb 662  u3lemnonb 663  u4lemnonb 664  u5lemnonb 665  u3lem1n 727  u4lem1n 728  u5lem1n 729  u4lem3n 741  u5lem3n 742  u3lem12 774  i1abs 787  test2 789  2oath1 812  elimconslem 853  elimcons 854  mlaconjo 872  oa6todual 938  oa8todual 957  oal1 986

Copyright terms: Public domain