Theorem necon3bbii 2870

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 214	. . 3 ⊢ (𝐴 = 𝐵 ↔ 𝜑)
3	2	necon3abii 2869	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑)
4	3	bicomi 214	1 ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 196   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necon1abii  2871  nssinpss  3889  difsnpss  4370  xpdifid  5597  wfi  5751  ordintdif  5812  tfi  7095  oelim2  7720  0sdomg  8130  fin23lem26  9185  axdc3lem4  9313  axdc4lem  9315  axcclem  9317  crreczi  13029  ef0lem  14853  lidlnz  19276  nconnsubb  21274  ufileu  21770  itg2cnlem1  23573  plyeq0lem  24011  abelthlem2  24231  ppinprm  24923  chtnprm  24925  ltgov  25537  usgr2pthlem  26715  shne0i  28435  pjneli  28710  eleigvec  28944  nmo  29453  qqhval2lem  30153  qqhval2  30154  sibfof  30530  dffr5  31769  frpoind  31865  frind  31868  ellimits  32142  elicc3  32436  itg2addnclem2  33592  ftc1anclem3  33617  onfrALTlem5  39074  onfrALTlem5VD  39435  limcrecl  40179