Theorem necon3abii 2985

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2938

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 206  df-ne 2939

This theorem is referenced by:  necon3bbii  2986  necon3bii  2991  nesym  2995  rabn0  4384  dffr6  5633  xpimasn  6183  rankxplim3  9878  rankxpsuc  9879  dflt2  13131  gcd0id  16464  lcmfunsnlem2  16581  axlowdimlem13  28479  hashxpe  32286  ssmxidllem  32863  fedgmullem2  33003  gonanegoal  34641  filnetlem4  35569  dihatlat  40508  sn-00id  41576  pellex  41875  nev  42823  ldepspr  47241