Theorem necon3abii 3062

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1533   ≠ wne 3016

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 3017

This theorem is referenced by:  necon3bbii  3063  necon3bii  3068  nesym  3072  rabn0  4339  xpimasn  6037  rankxplim3  9304  rankxpsuc  9305  dflt2  12535  gcd0id  15861  lcmfunsnlem2  15978  axlowdimlem13  26734  hashxpe  30523  ssmxidllem  30973  fedgmullem2  31021  gonanegoal  32594  filnetlem4  33724  dihatlat  38464  pellex  39425  nev  40108  ldepspr  44521