Theorem necon3bid 2417

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

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

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 2377

This theorem is referenced by:  nebidc  2456  addneintrd  8260  addneintr2d  8261  negne0bd  8376  negned  8380  subne0d  8392  subne0ad  8394  subneintrd  8427  subneintr2d  8429  qapne  9760  xrlttri3  9919  xaddass2  9992  seqf1oglem1  10664  sqne0  10750  fihashneq0  10939  hashnncl  10940  ccat1st1st  11093  cjne0  11219  absne0d  11498  sqrt2irraplemnn  12501  4sqlem11  12724  ringinvnz1ne0  13811  metn0  14850  perfectlem2  15472  lgsabs1  15516  neap0mkv  16008