Theorem necon3abii 3003

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2958

This theorem is used by:  necon3bbii  3004  necon3bii  3009  nesym  3013  rabn0  4342  dffr6  5615  xpimasn  6182  rankxplim3  9867  rankxpsuc  9868  dflt2  13203  gcd0id  16615  lcmfunsnlem2  16736  ssdifidllem  21553  axlowdimlem13  29419  hashxpe  33286  ssmxidllem  33884  fedgmullem2  34148  gonanegoal  35939  filnetlem4  37008  dihatlat  42215  sn-00id  43284  pellex  43684  nev  44618  ldepspr  49411