Theorem necon3abii 3002

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1559   ≠ wne 2956

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 2957

This theorem is referenced by:  necon3bbii  3003  necon3bii  3008  nesym  3012  rabn0  4342  dffr6  5601  xpimasn  6167  rankxplim3  9836  rankxpsuc  9837  dflt2  13147  gcd0id  16536  lcmfunsnlem2  16657  axlowdimlem13  29101  hashxpe  32959  ssdifidllem  33604  ssmxidllem  33622  fedgmullem2  33888  gonanegoal  35666  filnetlem4  36705  dihatlat  41922  sn-00id  42974  pellex  43376  nev  44310  ldepspr  49059