Theorem necon3abii 3002

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

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

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 2957

This theorem is used by:  necon3bbii  3003  necon3bii  3008  nesym  3012  rabn0  4339  dffr6  5607  xpimasn  6176  rankxplim3  9879  rankxpsuc  9880  dflt2  13258  gcd0id  16671  lcmfunsnlem2  16795  ssdifidllem  21620  axlowdimlem13  29514  hashxpe  33381  ssmxidllem  33980  fedgmullem2  34244  gonanegoal  36086  filnetlem4  37139  dihatlat  42359  sn-00id  43420  pellex  43795  nev  44729  ldepspr  49529