Theorem necon3bbii 2976

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  necon1abii  2977  nssinpss  4216  difsnpss  4758  xpdifid  6120  frpoind  6294  ordintdif  6362  tfi  7789  oelim2  8516  0sdomg  9026  frind  9650  fin23lem26  10223  axdc3lem4  10351  axdc4lem  10353  axcclem  10355  crreczi  14137  ef0lem  15987  lidlnz  21181  nconnsubb  23339  ufileu  23835  itg2cnlem1  25690  plyeq0lem  26143  abelthlem2  26370  ppinprm  27090  chtnprm  27092  sltlpss  27854  mulsval  28049  ltgov  28576  usgr2pthlem  29743  shne0i  31430  pjneli  31705  eleigvec  31939  nmo  32471  qqhval2lem  34015  qqhval2  34016  sibfof  34374  onvf1odlem2  35169  dffr5  35819  ellimits  35973  elicc3  36382  itg2addnclem2  37732  ftc1anclem3  37755  onfrALTlem5  44659  onfrALTlem5VD  45001  limcrecl  45753  dfnbgr6  47981