Theorem conb 122

Description: Contraposition law.

Assertion

Ref	Expression
conb	(a == b) = (a' == b')

Proof of Theorem conb

Step	Hyp	Ref	Expression
1		ax-a2 31	. . 3 ((a ^ b) v (a' ^ b')) = ((a' ^ b') v (a ^ b))
2		ax-a1 30	. . . . 5 a = a''
3		ax-a1 30	. . . . 5 b = b''
4	2, 3	2an 79	. . . 4 (a ^ b) = (a'' ^ b'')
5	4	lor 70	. . 3 ((a' ^ b') v (a ^ b)) = ((a' ^ b') v (a'' ^ b''))
6	1, 5	ax-r2 36	. 2 ((a ^ b) v (a' ^ b')) = ((a' ^ b') v (a'' ^ b''))
7		dfb 94	. 2 (a == b) = ((a ^ b) v (a' ^ b'))
8		dfb 94	. 2 (a' == b') = ((a' ^ b') v (a'' ^ b''))
9	6, 7, 8	3tr1 63	1 (a == b) = (a' == b')

Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7

This theorem is referenced by:  di 126  wr4 199  wcon 202  wcon1 207  wcon2 208  wwfh3 218  wwfh4 219  ka4lem 229  ska3 232  nomcon5 306  nom55 336  wom2 434  u3lemax4 796  comanbn 873

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-b 39  df-a 40

Copyright terms: Public domain