Theorem necon3abii 2990

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2943

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 2944

This theorem is referenced by:  necon3bbii  2991  necon3bii  2996  nesym  3000  rabn0  4319  dffr6  5547  xpimasn  6088  rankxplim3  9639  rankxpsuc  9640  dflt2  12882  gcd0id  16226  lcmfunsnlem2  16345  axlowdimlem13  27322  hashxpe  31127  ssmxidllem  31641  fedgmullem2  31711  gonanegoal  33314  filnetlem4  34570  dihatlat  39348  pellex  40657  nev  41378  ldepspr  45814