Theorem necon3abii 2972

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2926

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 2927

This theorem is referenced by:  necon3bbii  2973  necon3bii  2978  nesym  2982  rabn0  4354  dffr6  5596  xpimasn  6160  rankxplim3  9840  rankxpsuc  9841  dflt2  13114  gcd0id  16495  lcmfunsnlem2  16616  axlowdimlem13  28887  hashxpe  32738  ssdifidllem  33433  ssmxidllem  33450  fedgmullem2  33632  gonanegoal  35339  filnetlem4  36364  dihatlat  41323  sn-00id  42384  pellex  42816  nev  43752  ldepspr  48452