Theorem necon3abii 2986

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1541   ≠ wne 2939

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 2940

This theorem is referenced by:  necon3bbii  2987  necon3bii  2992  nesym  2996  rabn0  4350  dffr6  5596  xpimasn  6142  rankxplim3  9826  rankxpsuc  9827  dflt2  13077  gcd0id  16410  lcmfunsnlem2  16527  axlowdimlem13  27966  hashxpe  31779  ssmxidllem  32314  fedgmullem2  32412  gonanegoal  34033  filnetlem4  34929  dihatlat  39870  sn-00id  40928  pellex  41216  nev  42164  ldepspr  46674