Theorem com2an 484

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 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' v c')
6		df-a 40	. . . . 5 (b ^ c) = (b' v c')'
7	6	con2 67	. . . 4 (b ^ c)' = (b' v c')
8	7	ax-r1 35	. . 3 (b' v 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   v wo 6   ^ wa 7

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 1079

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

Copyright terms: Public domain