Theorem necon3abii 2993

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1550   ≠ wne 2947

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 2948

This theorem is referenced by:  necon3bbii  2994  necon3bii  2999  nesym  3003  rabn0  4333  dffr6  5592  xpimasn  6156  rankxplim3  9825  rankxpsuc  9826  dflt2  13136  gcd0id  16525  lcmfunsnlem2  16646  axlowdimlem13  29090  hashxpe  32948  ssdifidllem  33588  ssmxidllem  33605  fedgmullem2  33871  gonanegoal  35640  filnetlem4  36679  dihatlat  41896  sn-00id  42948  pellex  43350  nev  44284  ldepspr  49033