Theorem necon3abii 3006

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1563   ≠ wne 2960

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 2961

This theorem is referenced by:  necon3bbii  3007  necon3bii  3012  nesym  3016  rabn0  4346  dffr6  5608  xpimasn  6175  rankxplim3  9841  rankxpsuc  9842  dflt2  13164  gcd0id  16567  lcmfunsnlem2  16688  ssdifidllem  21444  axlowdimlem13  29213  hashxpe  33064  ssmxidllem  33673  fedgmullem2  33937  gonanegoal  35715  filnetlem4  36754  dihatlat  41970  sn-00id  43022  pellex  43424  nev  44358  ldepspr  49104