Theorem com2an 484

Description: Thm. 4.2 Beran p. 49. (Contributed by NM, 7-Nov-1997.)

Hypotheses

Ref	Expression
fh.1	a C b
fh.2	a C c

Assertion

Ref	Expression
com2an	a C (b ∩ c)

Proof of Theorem com2an

Step	Hyp	Ref	Expression
1		fh.1	. . . . 5 a C b
2	1	comcom4 455	. . . 4 a⊥ C b⊥
3		fh.2	. . . . 5 a C c
4	3	comcom4 455	. . . 4 a⊥ C c⊥
5	2, 4	com2or 483	. . 3 a⊥ C (b⊥ ∪ c⊥ )
6		df-a 40	. . . . 5 (b ∩ c) = (b⊥ ∪ c⊥ )⊥
7	6	con2 67	. . . 4 (b ∩ c)⊥ = (b⊥ ∪ c⊥ )
8	7	ax-r1 35	. . 3 (b⊥ ∪ c⊥ ) = (b ∩ c)⊥
9	5, 8	cbtr 182	. 2 a⊥ C (b ∩ c)⊥
10	9	comcom5 458	1 a C (b ∩ c)

Syntax hints:   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  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

This theorem is referenced by:  gsth2  490  dfi3b  499  oi3ai3  503  i3lem1  504  com2i3  509  i3con  551  i3orlem7  558  i3orlem8  559  ud1lem3  562  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1d  569  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud4lem3b  584  ud4lem3  585  ud5lem1a  586  ud5lem1b  587  ud5lem1  589  ud5lem3a  591  ud5lem3b  592  ud5lem3  594  u3lemaa  602  u4lemaa  603  u3lemana  607  u4lemana  608  u3lemab  612  u3lemanb  617  u4lemanb  618  u4lemona  628  u3lemob  632  u3lemonb  637  u4lemc1  683  u1lemc2  686  u2lemc2  687  u4lemc2  689  u5lemc2  690  u4lemle2  718  u5lembi  725  u4lem1  737  u4lem5  764  u4lem6  768  u1lem8  776  u1lem11  780  u3lem13a  789  u3lem13b  790  u3lem15  795  test  802  test2  803  3vded21  817  1oa  820  bi3  839  mlaconj4  844  neg3antlem2  865  comanblem1  870  mhlem  876  govar  896  lem4.6.2e1  1082