Theorem necon3bid 2441

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

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

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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117  df-ne 2401

This theorem is referenced by:  nebidc  2480  addneintrd  8345  addneintr2d  8346  negne0bd  8461  negned  8465  subne0d  8477  subne0ad  8479  subneintrd  8512  subneintr2d  8514  qapne  9846  xrlttri3  10005  xaddass2  10078  seqf1oglem1  10753  sqne0  10839  fihashneq0  11028  hashnncl  11029  ccat1st1st  11187  pfxn0  11235  cjne0  11434  absne0d  11713  sqrt2irraplemnn  12716  4sqlem11  12939  ringinvnz1ne0  14027  metn0  15067  perfectlem2  15689  lgsabs1  15733  umgrclwwlkge2  16139  neap0mkv  16497