Theorem necon3abii 2977

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1539   ≠ wne 2931

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 2932

This theorem is referenced by:  necon3bbii  2978  necon3bii  2983  nesym  2987  rabn0  4369  dffr6  5620  xpimasn  6185  rankxplim3  9903  rankxpsuc  9904  dflt2  13172  gcd0id  16538  lcmfunsnlem2  16659  axlowdimlem13  28899  hashxpe  32750  ssdifidllem  33419  ssmxidllem  33436  fedgmullem2  33616  gonanegoal  35316  filnetlem4  36341  dihatlat  41295  sn-00id  42394  pellex  42809  nev  43745  ldepspr  48348