Theorem necon3abii 3004

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  necon3bbii  3005  necon3bii  3010  nesym  3014  rabn0  4347  dffr6  5619  xpimasn  6185  rankxplim3  9854  rankxpsuc  9855  dflt2  13174  gcd0id  16578  lcmfunsnlem2  16699  ssdifidllem  21465  axlowdimlem13  29282  hashxpe  33130  ssmxidllem  33734  fedgmullem2  33998  gonanegoal  35822  filnetlem4  36870  dihatlat  42086  sn-00id  43140  pellex  43542  nev  44476  ldepspr  49230