Theorem necon3bbii 3003

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

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

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 2957

This theorem is used by:  necon1abii  3004  nssinpss  4213  difsnpss  4770  xpdifid  6158  frpoind  6338  ordintdif  6407  tfi  7853  oelim2  8588  0sdomg  9109  frind  9738  fin23lem26  10384  axdc3lem4  10512  axdc4lem  10514  axcclem  10516  crreczi  14352  ef0lem  16224  lidlnz  21510  nconnsubb  23721  ufileu  24218  itg2cnlem1  26062  plyeq0lem  26509  abelthlem2  26741  ppinprm  27461  chtnprm  27463  ltslpss  28276  mulsval  28477  ltgov  29042  usgr2pthlem  30331  shne0i  32032  pjneli  32307  eleigvec  32541  nmo  33068  qqhval2lem  34595  qqhval2  34596  sibfof  34955  onvf1odlem2  35856  ellimits  36642  elicc3  37075  itg2addnclem2  38558  ftc1anclem3  38581  onfrALTlem5  45484  onfrALTlem5VD  45826  limcrecl  46585  dfnbgr6  48899