Theorem necon3bbii 2989

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1542   ≠ wne 2941

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 206  df-ne 2942

This theorem is referenced by:  necon1abii  2990  nssinpss  4257  difsnpss  4811  xpdifid  6168  frpoind  6344  wfiOLD  6353  ordintdif  6415  tfi  7842  oelim2  8595  0sdomg  9104  0sdomgOLD  9105  frind  9745  fin23lem26  10320  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  crreczi  14191  ef0lem  16022  lidlnz  20853  nconnsubb  22927  ufileu  23423  itg2cnlem1  25279  plyeq0lem  25724  abelthlem2  25944  ppinprm  26656  chtnprm  26658  sltlpss  27401  mulsval  27565  ltgov  27848  usgr2pthlem  29020  shne0i  30701  pjneli  30976  eleigvec  31210  nmo  31730  qqhval2lem  32961  qqhval2  32962  sibfof  33339  dffr5  34724  ellimits  34882  elicc3  35202  itg2addnclem2  36540  ftc1anclem3  36563  onfrALTlem5  43303  onfrALTlem5VD  43646  limcrecl  44345