Theorem necon3bid 2455

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

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

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 2415

This theorem is referenced by:  nebidc  2494  suppval1  6452  addneintrd  8477  addneintr2d  8478  negne0bd  8593  negned  8597  subne0d  8609  subne0ad  8611  subneintrd  8644  subneintr2d  8646  qapne  9989  xrlttri3  10149  xaddass2  10222  seqf1oglem1  10905  sqne0  10991  fihashneq0  11182  hashnncl  11183  ccat1st1st  11354  pfxn0  11405  cjne0  11618  absne0d  11897  sqrt2irraplemnn  12901  4sqlem11  13124  ballotfilemfrcn0  13217  ringinvnz1ne0  14292  rrgsupp  14512  metn0  15369  perfectlem2  15994  lgsabs1  16038  umgrclwwlkge2  16523  neap0mkv  16981