Theorem necon3bbii 2986

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

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

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 2939

This theorem is referenced by:  necon1abii  2987  nssinpss  4255  difsnpss  4809  xpdifid  6166  frpoind  6342  wfiOLD  6351  ordintdif  6413  tfi  7844  oelim2  8597  0sdomg  9106  0sdomgOLD  9107  frind  9747  fin23lem26  10322  axdc3lem4  10450  axdc4lem  10452  axcclem  10454  crreczi  14195  ef0lem  16026  lidlnz  21002  nconnsubb  23147  ufileu  23643  itg2cnlem1  25511  plyeq0lem  25959  abelthlem2  26180  ppinprm  26892  chtnprm  26894  sltlpss  27638  mulsval  27804  ltgov  28115  usgr2pthlem  29287  shne0i  30968  pjneli  31243  eleigvec  31477  nmo  31997  qqhval2lem  33259  qqhval2  33260  sibfof  33637  dffr5  35028  ellimits  35186  elicc3  35505  itg2addnclem2  36843  ftc1anclem3  36866  onfrALTlem5  43605  onfrALTlem5VD  43948  limcrecl  44643