Theorem necon3bbii 2994

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon1abii  2995  nssinpss  4286  difsnpss  4832  xpdifid  6199  frpoind  6374  wfiOLD  6383  ordintdif  6445  tfi  7890  oelim2  8651  0sdomg  9170  0sdomgOLD  9171  frind  9819  fin23lem26  10394  axdc3lem4  10522  axdc4lem  10524  axcclem  10526  crreczi  14277  ef0lem  16126  lidlnz  21275  nconnsubb  23452  ufileu  23948  itg2cnlem1  25816  plyeq0lem  26269  abelthlem2  26494  ppinprm  27213  chtnprm  27215  sltlpss  27963  mulsval  28153  ltgov  28623  usgr2pthlem  29799  shne0i  31480  pjneli  31755  eleigvec  31989  nmo  32518  qqhval2lem  33927  qqhval2  33928  sibfof  34305  dffr5  35716  ellimits  35874  elicc3  36283  itg2addnclem2  37632  ftc1anclem3  37655  onfrALTlem5  44513  onfrALTlem5VD  44856  limcrecl  45550  dfnbgr6  47729