Theorem necon3bbii 3005

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  necon1abii  3006  nssinpss  4221  difsnpss  4776  xpdifid  6167  frpoind  6345  ordintdif  6414  tfi  7850  oelim2  8582  0sdomg  9095  frind  9723  fin23lem26  10310  axdc3lem4  10438  axdc4lem  10440  axcclem  10442  crreczi  14266  ef0lem  16133  lidlnz  21357  nconnsubb  23561  ufileu  24057  itg2cnlem1  25901  plyeq0lem  26348  abelthlem2  26573  ppinprm  27294  chtnprm  27296  ltslpss  28079  mulsval  28280  ltgov  28844  usgr2pthlem  30090  shne0i  31778  pjneli  32053  eleigvec  32287  nmo  32814  qqhval2lem  34349  qqhval2  34350  sibfof  34708  onvf1odlem2  35566  dffr5  36224  ellimits  36378  elicc3  36806  itg2addnclem2  38301  ftc1anclem3  38324  onfrALTlem5  45231  onfrALTlem5VD  45573  limcrecl  46325  dfnbgr6  48599