Theorem necon3bbii 2979

Description: Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)

Hypothesis

Ref	Expression
necon3bbii.1	⊢ (𝜑 ↔ 𝐴 = 𝐵)

Assertion

Ref	Expression
necon3bbii	⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)

Proof of Theorem necon3bbii

Step	Hyp	Ref	Expression
1		necon3bbii.1	. . . 4 ⊢ (𝜑 ↔ 𝐴 = 𝐵)
2	1	bicomi 224	. . 3 ⊢ (𝐴 = 𝐵 ↔ 𝜑)
3	2	necon3abii 2978	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
4	3	bicomi 224	1 ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  necon1abii  2980  nssinpss  4207  difsnpss  4752  xpdifid  6132  frpoind  6306  ordintdif  6374  tfi  7804  oelim2  8531  0sdomg  9044  frind  9674  fin23lem26  10247  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  crreczi  14190  ef0lem  16043  lidlnz  21240  nconnsubb  23388  ufileu  23884  itg2cnlem1  25728  plyeq0lem  26175  abelthlem2  26397  ppinprm  27115  chtnprm  27117  ltslpss  27900  mulsval  28101  ltgov  28665  usgr2pthlem  29831  shne0i  31519  pjneli  31794  eleigvec  32028  nmo  32559  qqhval2lem  34125  qqhval2  34126  sibfof  34484  onvf1odlem2  35286  dffr5  35936  ellimits  36090  elicc3  36499  itg2addnclem2  37993  ftc1anclem3  38016  onfrALTlem5  44969  onfrALTlem5VD  45311  limcrecl  46059  dfnbgr6  48333