Theorem necon3abii 2981

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1543   ≠ wne 2935

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 210  df-ne 2936

This theorem is referenced by:  necon3bbii  2982  necon3bii  2987  nesym  2991  rabn0  4290  xpimasn  6037  rankxplim3  9480  rankxpsuc  9481  dflt2  12721  gcd0id  16059  lcmfunsnlem2  16178  axlowdimlem13  27017  hashxpe  30819  ssmxidllem  31327  fedgmullem2  31397  gonanegoal  32999  filnetlem4  34264  dihatlat  39042  pellex  40312  nev  41007  ldepspr  45441