Theorem necon3bid 2444

Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

Ref	Expression
necon3bid.1	⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))

Assertion

Ref	Expression
necon3bid	⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Proof of Theorem necon3bid

Step	Hyp	Ref	Expression
1		df-ne 2404	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3bid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
3	2	necon3bbid 2443	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷))
4	1, 3	bitrid 192	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   = wceq 1398   ≠ wne 2403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117  df-ne 2404

This theorem is referenced by:  nebidc  2483  suppval1  6417  addneintrd  8409  addneintr2d  8410  negne0bd  8525  negned  8529  subne0d  8541  subne0ad  8543  subneintrd  8576  subneintr2d  8578  qapne  9917  xrlttri3  10076  xaddass2  10149  seqf1oglem1  10827  sqne0  10913  fihashneq0  11102  hashnncl  11103  ccat1st1st  11267  pfxn0  11318  cjne0  11531  absne0d  11810  sqrt2irraplemnn  12814  4sqlem11  13037  ringinvnz1ne0  14126  rrgsupp  14344  metn0  15172  perfectlem2  15797  lgsabs1  15841  umgrclwwlkge2  16326  neap0mkv  16785