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  8357  addneintr2d  8358  negne0bd  8473  negned  8477  subne0d  8489  subne0ad  8491  subneintrd  8524  subneintr2d  8526  qapne  9863  xrlttri3  10022  xaddass2  10095  seqf1oglem1  10771  sqne0  10857  fihashneq0  11046  hashnncl  11047  ccat1st1st  11208  pfxn0  11259  cjne0  11459  absne0d  11738  sqrt2irraplemnn  12741  4sqlem11  12964  ringinvnz1ne0  14052  metn0  15092  perfectlem2  15714  lgsabs1  15758  umgrclwwlkge2  16197  neap0mkv  16609