Theorem necon3bbii 3002

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

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

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 2956

This theorem is used by:  necon1abii  3003  nssinpss  4212  difsnpss  4766  xpdifid  6158  frpoind  6345  ordintdif  6414  tfi  7864  oelim2  8607  0sdomg  9128  frind  9757  fin23lem26  10406  axdc3lem4  10534  axdc4lem  10536  axcclem  10538  crreczi  14375  ef0lem  16249  lidlnz  21535  nconnsubb  23746  ufileu  24243  itg2cnlem1  26087  plyeq0lem  26534  abelthlem2  26764  ppinprm  27484  chtnprm  27486  ltslpss  28299  mulsval  28500  ltgov  29065  usgr2pthlem  30354  shne0i  32055  pjneli  32330  eleigvec  32564  nmo  33133  qqhval2lem  34659  qqhval2  34660  sibfof  35018  onvf1odlem2  35951  ellimits  36764  elicc3  37197  itg2addnclem2  38683  ftc1anclem3  38706  onfrALTlem5  45618  onfrALTlem5VD  45960  limcrecl  46734  dfnbgr6  49048