Theorem necon3abii 2978

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  necon3bbii  2979  necon3bii  2984  nesym  2988  rabn0  4329  dffr6  5587  xpimasn  6149  rankxplim3  9805  rankxpsuc  9806  dflt2  13099  gcd0id  16488  lcmfunsnlem2  16609  axlowdimlem13  29023  hashxpe  32880  ssdifidllem  33516  ssmxidllem  33533  fedgmullem2  33774  gonanegoal  35534  filnetlem4  36563  dihatlat  41780  sn-00id  42833  pellex  43263  nev  44197  ldepspr  48949