Theorem necon3abii 2975

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  necon3bbii  2976  necon3bii  2981  nesym  2985  rabn0  4338  dffr6  5575  xpimasn  6137  rankxplim3  9781  rankxpsuc  9782  dflt2  13049  gcd0id  16432  lcmfunsnlem2  16553  axlowdimlem13  28934  hashxpe  32794  ssdifidllem  33428  ssmxidllem  33445  fedgmullem2  33664  gonanegoal  35417  filnetlem4  36446  dihatlat  41453  sn-00id  42519  pellex  42952  nev  43887  ldepspr  48598