Theorem necon3bid 2461

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

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

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 623  ax-in2 624

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

This theorem is referenced by:  nebidc  2500  suppval1  6469  addneintrd  8504  addneintr2d  8505  negne0bd  8620  negned  8624  subne0d  8636  subne0ad  8638  subneintrd  8671  subneintr2d  8673  qapne  10018  xrlttri3  10178  xaddass2  10251  seqf1oglem1  10934  sqne0  11020  fihashneq0  11211  hashnncl  11212  ccat1st1st  11387  pfxn0  11438  cjne0  11652  absne0d  11931  sqrt2irraplemnn  12935  4sqlem11  13158  ballotfilemfrcn0  13251  ringinvnz1ne0  14327  rrgsupp  14547  metn0  15402  perfectlem2  16028  lgsabs1  16072  umgrclwwlkge2  16557  neap0mkv  17024