Theorem necon3abii 3064

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  necon3bbii  3065  necon3bii  3070  nesym  3074  rabn0  4341  xpimasn  6044  rankxplim3  9312  rankxpsuc  9313  dflt2  12544  gcd0id  15869  lcmfunsnlem2  15986  axlowdimlem13  26742  hashxpe  30531  ssmxidllem  30980  fedgmullem2  31028  gonanegoal  32601  filnetlem4  33731  dihatlat  38472  pellex  39439  nev  40122  ldepspr  44535