Theorem comcom5 458

Description: Commutation equivalence. Kalmbach 83 p. 23.

Hypothesis

Ref	Expression
comcom5.1	a' C b'

Assertion

Ref	Expression
comcom5	a C b

Proof of Theorem comcom5

Step	Hyp	Ref	Expression
1		comcom5.1	. . . . 5 a' C b'
2	1	comcom4 455	. . . 4 a'' C b''
3	2	df-c2 133	. . 3 a'' = ((a'' ^ b'') v (a'' ^ b'''))
4		ax-a1 30	. . 3 a = a''
5		ax-a1 30	. . . . 5 b = b''
6	4, 5	2an 79	. . . 4 (a ^ b) = (a'' ^ b'')
7		ax-a1 30	. . . . 5 b' = b'''
8	4, 7	2an 79	. . . 4 (a ^ b') = (a'' ^ b''')
9	6, 8	2or 72	. . 3 ((a ^ b) v (a ^ b')) = ((a'' ^ b'') v (a'' ^ b'''))
10	3, 4, 9	3tr1 63	. 2 a = ((a ^ b) v (a ^ b'))
11	10	df-c1 132	1 a C b

Syntax hints:   C wc 3  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  comcom6 459  comcom7 460  comdr 466  df2c1 468  com2an 484  oml4 487  gstho 491  df2i3 498  i3lem2 505  comi31 508  ud1lem1 560  ud1lem3 562  ud4lem1a 577  ud4lem1b 578  ud4lem1c 579  ud4lem1d 580  ud4lem1 581  ud5lem1a 586

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