Theorem necon3bbii 3007

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 227	. . 3 ⊢ (𝐴 = 𝐵 ↔ 𝜑)
3	2	necon3abii 3006	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
4	3	bicomi 227	1 ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1563   ≠ wne 2960

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 2961

This theorem is referenced by:  necon1abii  3008  nssinpss  4222  difsnpss  4770  xpdifid  6157  frpoind  6333  ordintdif  6401  tfi  7837  oelim2  8569  0sdomg  9082  frind  9710  fin23lem26  10297  axdc3lem4  10425  axdc4lem  10427  axcclem  10429  crreczi  14255  ef0lem  16122  lidlnz  21341  nconnsubb  23541  ufileu  24037  itg2cnlem1  25881  plyeq0lem  26328  abelthlem2  26553  ppinprm  27274  chtnprm  27276  ltslpss  28059  mulsval  28260  ltgov  28824  usgr2pthlem  30021  shne0i  31709  pjneli  31984  eleigvec  32218  nmo  32746  qqhval2lem  34288  qqhval2  34289  sibfof  34647  onvf1odlem2  35459  dffr5  36117  ellimits  36271  elicc3  36690  itg2addnclem2  38183  ftc1anclem3  38206  onfrALTlem5  45116  onfrALTlem5VD  45458  limcrecl  46203  dfnbgr6  48477