Theorem necon3bbii 3063

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1537   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  necon1abii  3064  nssinpss  4233  difsnpss  4740  xpdifid  6025  wfi  6181  ordintdif  6240  tfi  7568  oelim2  8221  0sdomg  8646  fin23lem26  9747  axdc3lem4  9875  axdc4lem  9877  axcclem  9879  crreczi  13590  ef0lem  15432  lidlnz  20001  nconnsubb  22031  ufileu  22527  itg2cnlem1  24362  plyeq0lem  24800  abelthlem2  25020  ppinprm  25729  chtnprm  25731  ltgov  26383  usgr2pthlem  27544  shne0i  29225  pjneli  29500  eleigvec  29734  nmo  30254  qqhval2lem  31222  qqhval2  31223  sibfof  31598  dffr5  32989  frpoind  33080  frind  33085  ellimits  33371  elicc3  33665  itg2addnclem2  34959  ftc1anclem3  34984  onfrALTlem5  40896  onfrALTlem5VD  41239  limcrecl  41930