Theorem necon3bid 2416

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 2376	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3bid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
3	2	necon3bbid 2415	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷))
4	1, 3	bitrid 192	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

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

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 615  ax-in2 616

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

This theorem is referenced by:  nebidc  2455  addneintrd  8259  addneintr2d  8260  negne0bd  8375  negned  8379  subne0d  8391  subne0ad  8393  subneintrd  8426  subneintr2d  8428  qapne  9759  xrlttri3  9918  xaddass2  9991  seqf1oglem1  10662  sqne0  10748  fihashneq0  10937  hashnncl  10938  ccat1st1st  11091  cjne0  11190  absne0d  11469  sqrt2irraplemnn  12472  4sqlem11  12695  ringinvnz1ne0  13782  metn0  14821  perfectlem2  15443  lgsabs1  15487  neap0mkv  15970