Theorem neeq1 1194

Description: Equality theorem for inequality.

Assertion

Ref	Expression
neeq1	⊢ (A = B → (A ≠ C ↔ B ≠ C))

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		cleq1 1107	. . 3 ⊢ (A = B → (A = C ↔ B = C))
2	1	negbid 463	. 2 ⊢ (A = B → (¬ A = C ↔ ¬ B = C))
3		df-ne 1192	. 2 ⊢ (A ≠ C ↔ ¬ A = C)
4		df-ne 1192	. 2 ⊢ (B ≠ C ↔ ¬ B = C)
5	2, 3, 4	3bitr4g 428	1 ⊢ (A = B → (A ≠ C ↔ B ≠ C))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   = wceq 1091   ≠ wne 1190

This theorem is referenced by:  neeq1d 1196  psseq1 1559  axrecex 4079  axrrecex 4081  elimne0 4102  mulcant 4208  divmult 4220  divclt 4223  divcan1t 4228  divcan2t 4229  recidt 4235  divrect 4238  divdistrt 4246  divcan3t 4251  dividt 4256  recrect 4260  redivclt 4276  gt0ne0t 4346  qrecclt 4646

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097  df-ne 1192

metamath.org