Theorem necon3bid 2419

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

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

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 2379

This theorem is referenced by:  nebidc  2458  addneintrd  8295  addneintr2d  8296  negne0bd  8411  negned  8415  subne0d  8427  subne0ad  8429  subneintrd  8462  subneintr2d  8464  qapne  9795  xrlttri3  9954  xaddass2  10027  seqf1oglem1  10701  sqne0  10787  fihashneq0  10976  hashnncl  10977  ccat1st1st  11131  pfxn0  11179  cjne0  11334  absne0d  11613  sqrt2irraplemnn  12616  4sqlem11  12839  ringinvnz1ne0  13926  metn0  14965  perfectlem2  15587  lgsabs1  15631  neap0mkv  16210