Theorem neeq1 2295

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)

Assertion

Ref	Expression
neeq1	⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		eqeq1 2121	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	notbid 639	. 2 ⊢ (𝐴 = 𝐵 → (¬ 𝐴 = 𝐶 ↔ ¬ 𝐵 = 𝐶))
3		df-ne 2283	. 2 ⊢ (𝐴 ≠ 𝐶 ↔ ¬ 𝐴 = 𝐶)
4		df-ne 2283	. 2 ⊢ (𝐵 ≠ 𝐶 ↔ ¬ 𝐵 = 𝐶)
5	2, 3, 4	3bitr4g 222	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104   = wceq 1314   ≠ wne 2282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-ne 2283

This theorem is referenced by:  neeq1i  2297  neeq1d  2300  nelrdva  2860  disji2  3888  0inp0  4050  frecabcl  6250  fiintim  6770  eldju2ndl  6909  updjudhf  6916  xnn0nemnf  8955  uzn0  9243  xrnemnf  9457  xrnepnf  9458  ngtmnft  9493  xsubge0  9557  xposdif  9558  xleaddadd  9563  fztpval  9756  fiinopn  12014