Theorem necon3abii 2971

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  necon3bbii  2972  necon3bii  2977  nesym  2981  rabn0  4352  dffr6  5594  xpimasn  6158  rankxplim3  9834  rankxpsuc  9835  dflt2  13108  gcd0id  16489  lcmfunsnlem2  16610  axlowdimlem13  28881  hashxpe  32732  ssdifidllem  33427  ssmxidllem  33444  fedgmullem2  33626  gonanegoal  35339  filnetlem4  36369  dihatlat  41328  sn-00id  42389  pellex  42823  nev  43759  ldepspr  48462