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

Syntax hints:  ¬ wn 3   ↔ wb 196   = wceq 1632   ≠ 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 197  df-ne 2933

This theorem is referenced by:  necon1abii  2980  nssinpss  3999  difsnpss  4483  xpdifid  5720  wfi  5874  ordintdif  5935  tfi  7218  oelim2  7844  0sdomg  8254  fin23lem26  9339  axdc3lem4  9467  axdc4lem  9469  axcclem  9471  crreczi  13183  ef0lem  15008  lidlnz  19430  nconnsubb  21428  ufileu  21924  itg2cnlem1  23727  plyeq0lem  24165  abelthlem2  24385  ppinprm  25077  chtnprm  25079  ltgov  25691  usgr2pthlem  26869  shne0i  28616  pjneli  28891  eleigvec  29125  nmo  29634  qqhval2lem  30334  qqhval2  30335  sibfof  30711  dffr5  31950  frpoind  32046  frind  32049  ellimits  32323  elicc3  32617  itg2addnclem2  33775  ftc1anclem3  33800  onfrALTlem5  39259  onfrALTlem5VD  39620  limcrecl  40364