Theorem necon3bbii 2990

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

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

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 2943

This theorem is referenced by:  necon1abii  2991  nssinpss  4187  difsnpss  4737  xpdifid  6060  frpoind  6230  wfiOLD  6239  ordintdif  6300  tfi  7675  oelim2  8388  0sdomg  8842  frind  9439  fin23lem26  10012  axdc3lem4  10140  axdc4lem  10142  axcclem  10144  crreczi  13871  ef0lem  15716  lidlnz  20412  nconnsubb  22482  ufileu  22978  itg2cnlem1  24831  plyeq0lem  25276  abelthlem2  25496  ppinprm  26206  chtnprm  26208  ltgov  26862  usgr2pthlem  28032  shne0i  29711  pjneli  29986  eleigvec  30220  nmo  30739  qqhval2lem  31831  qqhval2  31832  sibfof  32207  dffr5  33627  sltlpss  34014  ellimits  34139  elicc3  34433  itg2addnclem2  35756  ftc1anclem3  35779  onfrALTlem5  42051  onfrALTlem5VD  42394  limcrecl  43060