Theorem comor1 461

Description: Commutation law.

Assertion

Ref	Expression
comor1	(a v b) C a

Proof of Theorem comor1

Step	Hyp	Ref	Expression
1		comorr 184	. 2 a C (a v b)
2	1	comcom 453	1 (a v b) C a

Syntax hints:   C wc 3   v wo 6

This theorem is referenced by:  comor2 462  oml6 488  dfi3b 499  i3con 551  i3orlem7 558  i3orlem8 559  ud1lem2 561  ud1lem3 562  ud3lem1a 566  ud3lem1b 567  ud3lem1c 568  ud3lem1d 569  ud3lem3d 575  ud3lem3 576  ud4lem1b 578  ud4lem1c 579  ud4lem1d 580  ud4lem1 581  ud4lem3b 584  ud4lem3 585  ud5lem1 589  ud5lem3 594  u4lemana 608  u4lemoa 623  u4lemona 628  u3lemob 632  u3lemonb 637  u4lemle2 718  u4lem1 737  u4lem5 764  u4lem6 768  u1lem8 776  u1lem11 780  u3lem11 786  u3lem15 795  bi1o1a 798  test 802  test2 803  neg3antlem2 865  elimconslem 867  elimcons 868  mhlemlem1 874  mhlem 876  mlaconjolem 885

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

Copyright terms: Public domain