Theorem com2an 466

Description: Th. 4.2 Beran p. 49.

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 437	. . . 4 a⊥ C b⊥
3		fh.2	. . . . 5 a C c
4	3	comcom4 437	. . . 4 a⊥ C c⊥
5	2, 4	com2or 465	. . 3 a⊥ C (b⊥ ∪ c⊥ )
6		df-a 39	. . . . 5 (b ∩ c) = (b⊥ ∪ c⊥ )⊥
7	6	con2 64	. . . 4 (b ∩ c)⊥ = (b⊥ ∪ c⊥ )
8	7	ax-r1 34	. . 3 (b⊥ ∪ c⊥ ) = (b ∩ c)⊥
9	5, 8	cbtr 174	. 2 a⊥ C (b ∩ c)⊥
10	9	comcom5 440	1 a C (b ∩ c)

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

This theorem is referenced by:  gsth2 472  dfi3b 481  oi3ai3 485  i3lem1 486  com2i3 491  i3con 533  i3orlem7 540  i3orlem8 541  ud1lem3 544  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem3b 566  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem1 571  ud5lem3a 573  ud5lem3b 574  ud5lem3 576  u3lemaa 584  u4lemaa 585  u3lemana 589  u4lemana 590  u3lemab 594  u3lemanb 599  u4lemanb 600  u4lemona 610  u3lemob 614  u3lemonb 619  u4lemc1 665  u1lemc2 668  u2lemc2 669  u4lemc2 671  u5lemc2 672  u4lemle2 700  u5lembi 707  u4lem1 719  u4lem5 746  u4lem6 750  u1lem8 758  u1lem11 762  u3lem13a 771  u3lem13b 772  u3lem15 777  test 784  test2 785  3vded21 799  1oa 802  bi3 821  mlaconj4 826  neg3antlem2 847  comanblem1 852  mhlem 858  govar 876

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org