Theorem necon3abii 2989

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

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

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 2943

This theorem is referenced by:  necon3bbii  2990  necon3bii  2995  nesym  2999  rabn0  4316  dffr6  5538  xpimasn  6077  rankxplim3  9570  rankxpsuc  9571  dflt2  12811  gcd0id  16154  lcmfunsnlem2  16273  axlowdimlem13  27225  hashxpe  31029  ssmxidllem  31543  fedgmullem2  31613  gonanegoal  33214  filnetlem4  34497  dihatlat  39275  pellex  40573  nev  41267  ldepspr  45702