Theorem necon3abii 2987

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1539   ≠ wne 2940

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 207  df-ne 2941

This theorem is referenced by:  necon3bbii  2988  necon3bii  2993  nesym  2997  rabn0  4398  dffr6  5648  xpimasn  6213  rankxplim3  9928  rankxpsuc  9929  dflt2  13196  gcd0id  16562  lcmfunsnlem2  16683  axlowdimlem13  28995  hashxpe  32831  ssdifidllem  33496  ssmxidllem  33513  fedgmullem2  33690  gonanegoal  35350  filnetlem4  36376  dihatlat  41331  sn-00id  42424  pellex  42839  nev  43776  ldepspr  48357