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  4343  dffr6  5588  xpimasn  6151  rankxplim3  9805  rankxpsuc  9806  dflt2  13074  gcd0id  16458  lcmfunsnlem2  16579  axlowdimlem13  29039  hashxpe  32897  ssdifidllem  33548  ssmxidllem  33565  fedgmullem2  33807  gonanegoal  35565  filnetlem4  36594  dihatlat  41704  sn-00id  42765  pellex  43186  nev  44120  ldepspr  48827