Theorem necon3abii 3005

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

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

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 2960

This theorem is used by:  necon3bbii  3006  necon3bii  3011  nesym  3015  rabn0  4342  dffr6  5612  xpimasn  6190  rankxplim3  9928  rankxpsuc  9929  dflt2  13307  gcd0id  16723  lcmfunsnlem2  16847  ssdifidllem  21673  axlowdimlem13  29565  hashxpe  33472  ssmxidllem  34082  fedgmullem2  34345  gonanegoal  36297  filnetlem4  37360  dihatlat  42594  sn-00id  43656  frlmnzcoordex  43856  pellex  44046  nev  44973  ldepspr  49800