Theorem necon3abii 2981

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

Syntax hints:  ¬ wn 3   ↔ wb 207   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon3bbii  2982  necon3bii  2987  nesym  2991  rabn0  4324  dffr6  5581  xpimasn  6143  rankxplim3  9803  rankxpsuc  9804  dflt2  13097  gcd0id  16486  lcmfunsnlem2  16607  axlowdimlem13  29048  hashxpe  32906  ssdifidllem  33546  ssmxidllem  33563  fedgmullem2  33821  gonanegoal  35587  filnetlem4  36616  dihatlat  41833  sn-00id  42885  pellex  43287  nev  44221  ldepspr  48971