Theorem necon3bbii 2975

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  necon1abii  2976  nssinpss  4217  difsnpss  4759  xpdifid  6115  frpoind  6289  ordintdif  6357  tfi  7783  oelim2  8510  0sdomg  9019  frind  9640  fin23lem26  10213  axdc3lem4  10341  axdc4lem  10343  axcclem  10345  crreczi  14132  ef0lem  15982  lidlnz  21177  nconnsubb  23336  ufileu  23832  itg2cnlem1  25687  plyeq0lem  26140  abelthlem2  26367  ppinprm  27087  chtnprm  27089  sltlpss  27851  mulsval  28046  ltgov  28573  usgr2pthlem  29739  shne0i  31423  pjneli  31698  eleigvec  31932  nmo  32464  qqhval2lem  33989  qqhval2  33990  sibfof  34348  onvf1odlem2  35136  dffr5  35786  ellimits  35943  elicc3  36350  itg2addnclem2  37711  ftc1anclem3  37734  onfrALTlem5  44574  onfrALTlem5VD  44916  limcrecl  45668  dfnbgr6  47887