Theorem necon3bbii 2829

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

Syntax hints:  ¬ wn 3   ↔ wb 195   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon1abii  2830  nssinpss  3818  difsnpss  4279  xpdifid  5481  wfi  5630  ordintdif  5691  tfi  6945  oelim2  7562  0sdomg  7974  fin23lem26  9030  axdc3lem4  9158  axdc4lem  9160  axcclem  9162  crreczi  12851  ef0lem  14648  lidlnz  19049  nconsubb  21036  ufileu  21533  itg2cnlem1  23334  plyeq0lem  23770  abelthlem2  23990  ppinprm  24678  chtnprm  24680  ltgov  25292  shne0i  27691  pjneli  27966  eleigvec  28200  nmo  28709  qqhval2lem  29353  qqhval2  29354  sibfof  29729  dffr5  30896  frind  30984  ellimits  31187  elicc3  31481  itg2addnclem2  32632  ftc1anclem3  32657  onfrALTlem5  37778  limcrecl  38696  usgr2pthlem  40969