Theorem necon3abii 3007

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

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

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 2962

This theorem is used by:  necon3bbii  3008  necon3bii  3013  nesym  3017  rabn0  4349  dffr6  5622  xpimasn  6188  rankxplim3  9863  rankxpsuc  9864  dflt2  13191  gcd0id  16602  lcmfunsnlem2  16723  ssdifidllem  21521  axlowdimlem13  29341  hashxpe  33189  ssmxidllem  33787  fedgmullem2  34051  gonanegoal  35865  filnetlem4  36933  dihatlat  42149  sn-00id  43203  pellex  43603  nev  44537  ldepspr  49294