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  8366  addneintr2d  8367  negne0bd  8482  negned  8486  subne0d  8498  subne0ad  8500  subneintrd  8533  subneintr2d  8535  qapne  9872  xrlttri3  10031  xaddass2  10104  seqf1oglem1  10780  sqne0  10866  fihashneq0  11055  hashnncl  11056  ccat1st1st  11217  pfxn0  11268  cjne0  11468  absne0d  11747  sqrt2irraplemnn  12750  4sqlem11  12973  ringinvnz1ne0  14061  metn0  15101  perfectlem2  15723  lgsabs1  15767  umgrclwwlkge2  16252  neap0mkv  16673