Theorem necon3bbii 3004

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2958

This theorem is used by:  necon1abii  3005  nssinpss  4216  difsnpss  4773  xpdifid  6164  frpoind  6344  ordintdif  6413  tfi  7853  oelim2  8587  0sdomg  9108  frind  9736  fin23lem26  10331  axdc3lem4  10459  axdc4lem  10461  axcclem  10463  crreczi  14296  ef0lem  16170  lidlnz  21445  nconnsubb  23654  ufileu  24151  itg2cnlem1  25995  plyeq0lem  26443  abelthlem2  26675  ppinprm  27396  chtnprm  27398  ltslpss  28181  mulsval  28382  ltgov  28947  usgr2pthlem  30236  shne0i  31937  pjneli  32212  eleigvec  32446  nmo  32973  qqhval2lem  34499  qqhval2  34500  sibfof  34859  onvf1odlem2  35709  ellimits  36495  elicc3  36944  itg2addnclem2  38429  ftc1anclem3  38452  onfrALTlem5  45373  onfrALTlem5VD  45715  limcrecl  46467  dfnbgr6  48781