Theorem necon3bbii 2980

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon1abii  2981  nssinpss  4221  difsnpss  4765  xpdifid  6134  frpoind  6308  ordintdif  6376  tfi  7805  oelim2  8533  0sdomg  9046  frind  9674  fin23lem26  10247  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  crreczi  14163  ef0lem  16013  lidlnz  21209  nconnsubb  23379  ufileu  23875  itg2cnlem1  25730  plyeq0lem  26183  abelthlem2  26410  ppinprm  27130  chtnprm  27132  ltslpss  27916  mulsval  28117  ltgov  28681  usgr2pthlem  29848  shne0i  31535  pjneli  31810  eleigvec  32044  nmo  32575  qqhval2lem  34158  qqhval2  34159  sibfof  34517  onvf1odlem2  35317  dffr5  35967  ellimits  36121  elicc3  36530  itg2addnclem2  37917  ftc1anclem3  37940  onfrALTlem5  44892  onfrALTlem5VD  45234  limcrecl  45983  dfnbgr6  48211