Theorem necon3bbii 2980

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  necon1abii  2981  nssinpss  4208  difsnpss  4751  xpdifid  6126  frpoind  6300  ordintdif  6368  tfi  7797  oelim2  8524  0sdomg  9037  frind  9665  fin23lem26  10238  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  crreczi  14181  ef0lem  16034  lidlnz  21232  nconnsubb  23398  ufileu  23894  itg2cnlem1  25738  plyeq0lem  26185  abelthlem2  26410  ppinprm  27129  chtnprm  27131  ltslpss  27914  mulsval  28115  ltgov  28679  usgr2pthlem  29846  shne0i  31534  pjneli  31809  eleigvec  32043  nmo  32574  qqhval2lem  34141  qqhval2  34142  sibfof  34500  onvf1odlem2  35302  dffr5  35952  ellimits  36106  elicc3  36515  itg2addnclem2  38007  ftc1anclem3  38030  onfrALTlem5  44987  onfrALTlem5VD  45329  limcrecl  46077  dfnbgr6  48345