Theorem an1 100

Description: Conjunction with 1.

Assertion

Ref	Expression
an1	(a ^ 1) = a

Proof of Theorem an1

Step	Hyp	Ref	Expression
1		df-a 40	. 2 (a ^ 1) = (a' v 1')'
2		df-f 42	. . . . . 6 0 = 1'
3	2	ax-r1 35	. . . . 5 1' = 0
4	3	lor 67	. . . 4 (a' v 1') = (a' v 0)
5		or0 96	. . . 4 (a' v 0) = a'
6	4, 5	ax-r2 36	. . 3 (a' v 1') = a'
7	6	con2 65	. 2 (a' v 1')' = a
8	1, 7	ax-r2 36	1 (a ^ 1) = a

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8  0wf 9

This theorem is referenced by:  an1r 101  1b 111  comm0 172  comm1 173  lei3 240  i3id 245  1i1 268  wql2lem5 286  wlem14 416  ska2 418  ska4 419  woml6 422  oml6 474  i3lem1 490  i3le 501  i3abs3 510  i3con 537  ud1lem1 546  ud1lem2 547  ud1lem3 548  ud2lem3 551  ud3lem1c 554  ud3lem1 556  ud3lem3 562  ud4lem1c 565  ud4lem1 567  ud4lem2 568  ud4lem3b 570  ud4lem3 571  ud5lem1 575  ud5lem3 580  u4lemoa 609  u4lemona 614  u3lemob 618  u4lemob 619  u3lemonb 623  u1lemc4 687  u2lemc4 688  u3lemc4 689  u4lemc4 690  u5lemc4 691  u1lemle2 701  u2lemle2 702  u4lemle2 704  u5lemle2 705  oi3oa3 719  u2lem3 736  u3lem3 737  u1lem4 743  u4lem4 745  u4lem5 750  u5lem5 751  u4lem6 754  u5lem6 755  u1lem11 766  u3lem10 771  u3lem11 772  u3lem13a 775  u3lem13b 776  u3lem14a 777  i1abs 787  test 788  test2 789  3vded12 801  3vded13 802  3vded3 805  3vroa 817  negantlem2 835  neg3antlem2 851  elimconslem 853  elimcons 854  mhlem1 863  oago3.29 875  gomaex3lem1 900  gomaex3lem2 901  gomaex3lem3 902  gomaex3lem7 906  oau 915  oa6v4v 919  oa23 922  oa3to4lem1 931  oa3to4lem2 932  oa4to6lem1 946  oa4to6lem2 947  oa4to6lem3 948  oa3-2lema 964  oa3-2lemb 965  oa3-6lem 966  oa3-3lem 967  oa3-1lem 968  oa3-4lem 969  oa3-5lem 970  oa3-u1lem 971  oa3-u2lem 972  oa3-6to3 973  oa3-2to4 974  oa3-2to2s 976  oa3-u1 977  oa3-u2 978  lem3.3.7i0e1 1042  lem3.3.7i1e2 1046  lem3.3.7i2e2 1049  lem3.3.7i3e1 1051  lem3.3.7i3e2 1052  lem3.3.7i4e1 1054  lem3.3.7i4e2 1055

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42

Copyright terms: Public domain