Theorem necon3bid 2443

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

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

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 2403

This theorem is referenced by:  nebidc  2482  addneintrd  8367  addneintr2d  8368  negne0bd  8483  negned  8487  subne0d  8499  subne0ad  8501  subneintrd  8534  subneintr2d  8536  qapne  9873  xrlttri3  10032  xaddass2  10105  seqf1oglem1  10782  sqne0  10868  fihashneq0  11057  hashnncl  11058  ccat1st1st  11222  pfxn0  11273  cjne0  11486  absne0d  11765  sqrt2irraplemnn  12769  4sqlem11  12992  ringinvnz1ne0  14081  metn0  15121  perfectlem2  15743  lgsabs1  15787  umgrclwwlkge2  16272  neap0mkv  16725