Theorem necon3bbii 2985

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1536   ≠ wne 2937

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 207  df-ne 2938

This theorem is referenced by:  necon1abii  2986  nssinpss  4272  difsnpss  4811  xpdifid  6189  frpoind  6364  wfiOLD  6373  ordintdif  6435  tfi  7873  oelim2  8631  0sdomg  9142  0sdomgOLD  9143  frind  9787  fin23lem26  10362  axdc3lem4  10490  axdc4lem  10492  axcclem  10494  crreczi  14263  ef0lem  16110  lidlnz  21269  nconnsubb  23446  ufileu  23942  itg2cnlem1  25810  plyeq0lem  26263  abelthlem2  26490  ppinprm  27209  chtnprm  27211  sltlpss  27959  mulsval  28149  ltgov  28619  usgr2pthlem  29795  shne0i  31476  pjneli  31751  eleigvec  31985  nmo  32517  qqhval2lem  33943  qqhval2  33944  sibfof  34321  dffr5  35733  ellimits  35891  elicc3  36299  itg2addnclem2  37658  ftc1anclem3  37681  onfrALTlem5  44539  onfrALTlem5VD  44882  limcrecl  45584  dfnbgr6  47780