Theorem necon3bbii 2982

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

Syntax hints:  ¬ wn 3   ↔ wb 207   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon1abii  2983  nssinpss  4202  difsnpss  4747  xpdifid  6126  frpoind  6300  ordintdif  6368  tfi  7800  oelim2  8528  0sdomg  9041  frind  9672  fin23lem26  10245  axdc3lem4  10373  axdc4lem  10375  axcclem  10377  crreczi  14188  ef0lem  16041  lidlnz  21242  nconnsubb  23413  ufileu  23909  itg2cnlem1  25753  plyeq0lem  26200  abelthlem2  26422  ppinprm  27140  chtnprm  27142  ltslpss  27925  mulsval  28126  ltgov  28690  usgr2pthlem  29856  shne0i  31544  pjneli  31819  eleigvec  32053  nmo  32584  qqhval2lem  34172  qqhval2  34173  sibfof  34531  onvf1odlem2  35339  dffr5  35989  ellimits  36143  elicc3  36552  itg2addnclem2  38046  ftc1anclem3  38069  onfrALTlem5  44993  onfrALTlem5VD  45335  limcrecl  46081  dfnbgr6  48355