Theorem necon3abii 2979

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon3bbii  2980  necon3bii  2985  nesym  2989  rabn0  4330  dffr6  5580  xpimasn  6143  rankxplim3  9796  rankxpsuc  9797  dflt2  13090  gcd0id  16479  lcmfunsnlem2  16600  axlowdimlem13  29037  hashxpe  32895  ssdifidllem  33531  ssmxidllem  33548  fedgmullem2  33790  gonanegoal  35550  filnetlem4  36579  dihatlat  41794  sn-00id  42847  pellex  43281  nev  44215  ldepspr  48961