Theorem necon3bbii 2979

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2932

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 2933

This theorem is referenced by:  necon1abii  2980  nssinpss  4242  difsnpss  4783  xpdifid  6157  frpoind  6331  wfiOLD  6340  ordintdif  6403  tfi  7848  oelim2  8607  0sdomg  9118  0sdomgOLD  9119  frind  9764  fin23lem26  10339  axdc3lem4  10467  axdc4lem  10469  axcclem  10471  crreczi  14246  ef0lem  16094  lidlnz  21203  nconnsubb  23361  ufileu  23857  itg2cnlem1  25714  plyeq0lem  26167  abelthlem2  26394  ppinprm  27114  chtnprm  27116  sltlpss  27871  mulsval  28064  ltgov  28576  usgr2pthlem  29745  shne0i  31429  pjneli  31704  eleigvec  31938  nmo  32471  qqhval2lem  34012  qqhval2  34013  sibfof  34372  dffr5  35771  ellimits  35928  elicc3  36335  itg2addnclem2  37696  ftc1anclem3  37719  onfrALTlem5  44567  onfrALTlem5VD  44909  limcrecl  45658  dfnbgr6  47870