Theorem necon3abii 2976

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 2930	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abii.1	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝜑)
3	1, 2	xchbinx 333	1 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1533   ≠ wne 2929

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 206  df-ne 2930

This theorem is referenced by:  necon3bbii  2977  necon3bii  2982  nesym  2986  rabn0  4387  dffr6  5636  xpimasn  6191  rankxplim3  9906  rankxpsuc  9907  dflt2  13162  gcd0id  16497  lcmfunsnlem2  16614  axlowdimlem13  28837  hashxpe  32659  ssdifidllem  33268  ssmxidllem  33285  fedgmullem2  33456  gonanegoal  35090  filnetlem4  35993  dihatlat  40934  sn-00id  42088  pellex  42394  nev  43339  ldepspr  47724