Theorem necon3bbii 2991

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 223	. . 3 ⊢ (𝐴 = 𝐵 ↔ 𝜑)
3	2	necon3abii 2990	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
4	3	bicomi 223	1 ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2943

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 206  df-ne 2944

This theorem is referenced by:  necon1abii  2992  nssinpss  4190  difsnpss  4740  xpdifid  6071  frpoind  6245  wfiOLD  6254  ordintdif  6315  tfi  7700  oelim2  8426  0sdomg  8891  0sdomgOLD  8892  frind  9508  fin23lem26  10081  axdc3lem4  10209  axdc4lem  10211  axcclem  10213  crreczi  13943  ef0lem  15788  lidlnz  20499  nconnsubb  22574  ufileu  23070  itg2cnlem1  24926  plyeq0lem  25371  abelthlem2  25591  ppinprm  26301  chtnprm  26303  ltgov  26958  usgr2pthlem  28131  shne0i  29810  pjneli  30085  eleigvec  30319  nmo  30838  qqhval2lem  31931  qqhval2  31932  sibfof  32307  dffr5  33721  sltlpss  34087  ellimits  34212  elicc3  34506  itg2addnclem2  35829  ftc1anclem3  35852  onfrALTlem5  42162  onfrALTlem5VD  42505  limcrecl  43170