Theorem necon3abii 2974

Description: Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)

Hypothesis

Ref	Expression
necon3abii.1	⊢ (𝐴 = 𝐵 ↔ 𝜑)

Assertion

Ref	Expression
necon3abii	⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)

Proof of Theorem necon3abii

Step	Hyp	Ref	Expression
1		df-ne 2929	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abii.1	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝜑)
3	1, 2	xchbinx 334	1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-ne 2929

This theorem is referenced by:  necon3bbii  2975  necon3bii  2980  nesym  2984  rabn0  4339  dffr6  5572  xpimasn  6132  rankxplim3  9771  rankxpsuc  9772  dflt2  13044  gcd0id  16427  lcmfunsnlem2  16548  axlowdimlem13  28930  hashxpe  32784  ssdifidllem  33416  ssmxidllem  33433  fedgmullem2  33638  gonanegoal  35384  filnetlem4  36414  dihatlat  41372  sn-00id  42433  pellex  42867  nev  43802  ldepspr  48504