Theorem necon3abii 2988

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  necon3bbii  2989  necon3bii  2994  nesym  2998  rabn0  4386  dffr6  5635  xpimasn  6185  rankxplim3  9876  rankxpsuc  9877  dflt2  13127  gcd0id  16460  lcmfunsnlem2  16577  axlowdimlem13  28212  hashxpe  32019  ssmxidllem  32589  fedgmullem2  32715  gonanegoal  34343  filnetlem4  35266  dihatlat  40205  sn-00id  41274  pellex  41573  nev  42521  ldepspr  47154