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 1541   ≠ 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  4219  difsnpss  4763  xpdifid  6126  frpoind  6300  ordintdif  6368  tfi  7795  oelim2  8523  0sdomg  9034  frind  9662  fin23lem26  10235  axdc3lem4  10363  axdc4lem  10365  axcclem  10367  crreczi  14151  ef0lem  16001  lidlnz  21197  nconnsubb  23367  ufileu  23863  itg2cnlem1  25718  plyeq0lem  26171  abelthlem2  26398  ppinprm  27118  chtnprm  27120  ltslpss  27904  mulsval  28105  ltgov  28669  usgr2pthlem  29836  shne0i  31523  pjneli  31798  eleigvec  32032  nmo  32564  qqhval2lem  34138  qqhval2  34139  sibfof  34497  onvf1odlem2  35298  dffr5  35948  ellimits  36102  elicc3  36511  itg2addnclem2  37869  ftc1anclem3  37892  onfrALTlem5  44779  onfrALTlem5VD  45121  limcrecl  45871  dfnbgr6  48099