Theorem necon3bid 2453

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

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

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 2413

This theorem is referenced by:  nebidc  2492  suppval1  6439  addneintrd  8461  addneintr2d  8462  negne0bd  8577  negned  8581  subne0d  8593  subne0ad  8595  subneintrd  8628  subneintr2d  8630  qapne  9971  xrlttri3  10130  xaddass2  10203  seqf1oglem1  10881  sqne0  10967  fihashneq0  11157  hashnncl  11158  ccat1st1st  11329  pfxn0  11380  cjne0  11593  absne0d  11872  sqrt2irraplemnn  12876  4sqlem11  13099  ringinvnz1ne0  14193  rrgsupp  14411  metn0  15243  perfectlem2  15868  lgsabs1  15912  umgrclwwlkge2  16397  neap0mkv  16855