Theorem necon3abii 3001

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon3bbii  3002  necon3bii  3007  nesym  3011  rabn0  4338  dffr6  5606  xpimasn  6176  rankxplim3  9901  rankxpsuc  9902  dflt2  13280  gcd0id  16696  lcmfunsnlem2  16820  ssdifidllem  21645  axlowdimlem13  29537  hashxpe  33445  ssmxidllem  34044  fedgmullem2  34308  gonanegoal  36203  filnetlem4  37261  dihatlat  42484  sn-00id  43545  frlmnzcoordex  43745  pellex  43935  nev  44863  ldepspr  49678