Theorem necon3bbii 3009

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

Syntax hints:  ¬ wn 3   ↔ wb 198   = wceq 1508   ≠ wne 2962

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 199  df-ne 2963

This theorem is referenced by:  necon1abii  3010  nssinpss  4115  difsnpss  4611  xpdifid  5863  wfi  6017  ordintdif  6076  tfi  7383  oelim2  8021  0sdomg  8441  fin23lem26  9544  axdc3lem4  9672  axdc4lem  9674  axcclem  9676  crreczi  13403  ef0lem  15291  lidlnz  19735  nconnsubb  21751  ufileu  22247  itg2cnlem1  24081  plyeq0lem  24519  abelthlem2  24739  ppinprm  25447  chtnprm  25449  ltgov  26101  usgr2pthlem  27268  shne0i  29022  pjneli  29297  eleigvec  29531  nmo  30052  qqhval2lem  30899  qqhval2  30900  sibfof  31276  dffr5  32542  frpoind  32634  frind  32639  ellimits  32925  elicc3  33219  itg2addnclem2  34418  ftc1anclem3  34443  onfrALTlem5  40329  onfrALTlem5VD  40672  limcrecl  41371