Theorem an1 106

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 70	. . . 4 (a' v 1') = (a' v 0)
5		or0 102	. . . 4 (a' v 0) = a'
6	4, 5	ax-r2 36	. . 3 (a' v 1') = a'
7	6	con2 67	. 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 107  1b 117  comm0 178  comm1 179  lei3 246  i3id 251  1i1 274  wql2lem5 292  wlem14 430  ska2 432  ska4 433  woml6 436  oml6 488  i3lem1 504  i3le 515  i3abs3 524  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  u4lemoa 623  u4lemona 628  u3lemob 632  u4lemob 633  u3lemonb 637  u1lemc4 701  u2lemc4 702  u3lemc4 703  u4lemc4 704  u5lemc4 705  u1lemle2 715  u2lemle2 716  u4lemle2 718  u5lemle2 719  oi3oa3 733  u2lem3 750  u3lem3 751  u1lem4 757  u4lem4 759  u4lem5 764  u5lem5 765  u4lem6 768  u5lem6 769  u1lem11 780  u3lem10 785  u3lem11 786  u3lem13a 789  u3lem13b 790  u3lem14a 791  i1abs 801  test 802  test2 803  3vded12 815  3vded13 816  3vded3 819  3vroa 831  negantlem2 849  neg3antlem2 865  elimconslem 867  elimcons 868  mhlem1 877  oago3.29 889  gomaex3lem1 914  gomaex3lem2 915  gomaex3lem3 916  gomaex3lem7 920  oau 929  oa6v4v 933  oa23 936  oa3to4lem1 945  oa3to4lem2 946  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  oa3-2lema 978  oa3-2lemb 979  oa3-6lem 980  oa3-3lem 981  oa3-1lem 982  oa3-4lem 983  oa3-5lem 984  oa3-u1lem 985  oa3-u2lem 986  oa3-6to3 987  oa3-2to4 988  oa3-2to2s 990  oa3-u1 991  oa3-u2 992  lem3.3.7i0e1 1056  lem3.3.7i1e2 1060  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069

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