Theorem necon3abii 2978

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

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

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 2933

This theorem is referenced by:  necon3bbii  2979  necon3bii  2984  nesym  2988  rabn0  4341  dffr6  5580  xpimasn  6143  rankxplim3  9793  rankxpsuc  9794  dflt2  13062  gcd0id  16446  lcmfunsnlem2  16567  axlowdimlem13  29027  hashxpe  32887  ssdifidllem  33537  ssmxidllem  33554  fedgmullem2  33787  gonanegoal  35546  filnetlem4  36575  dihatlat  41590  sn-00id  42652  pellex  43073  nev  44007  ldepspr  48715