Theorem necon3bbii 2973

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

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

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 2927

This theorem is referenced by:  necon1abii  2974  nssinpss  4233  difsnpss  4774  xpdifid  6144  frpoind  6318  ordintdif  6386  tfi  7832  oelim2  8562  0sdomg  9076  frind  9710  fin23lem26  10285  axdc3lem4  10413  axdc4lem  10415  axcclem  10417  crreczi  14200  ef0lem  16051  lidlnz  21159  nconnsubb  23317  ufileu  23813  itg2cnlem1  25669  plyeq0lem  26122  abelthlem2  26349  ppinprm  27069  chtnprm  27071  sltlpss  27826  mulsval  28019  ltgov  28531  usgr2pthlem  29700  shne0i  31384  pjneli  31659  eleigvec  31893  nmo  32426  qqhval2lem  33978  qqhval2  33979  sibfof  34338  onvf1odlem2  35098  dffr5  35748  ellimits  35905  elicc3  36312  itg2addnclem2  37673  ftc1anclem3  37696  onfrALTlem5  44539  onfrALTlem5VD  44881  limcrecl  45634  dfnbgr6  47861