Theorem necon3abii 3014

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

Syntax hints:  ¬ wn 3   ↔ wb 198   = wceq 1601   ≠ wne 2968

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 199  df-ne 2969

This theorem is referenced by:  necon3bbii  3015  necon3bii  3020  nesym  3024  rabn0  4187  xpimasn  5833  rankxplim3  9041  rankxpsuc  9042  dflt2  12291  gcd0id  15646  lcmfunsnlem2  15759  axlowdimlem13  26303  filnetlem4  32978  dihatlat  37482  pellex  38351  nev  39011  ldepspr  43269