Theorem necon3bbii 2988

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  necon1abii  2989  nssinpss  4267  difsnpss  4807  xpdifid  6188  frpoind  6363  wfiOLD  6372  ordintdif  6434  tfi  7874  oelim2  8633  0sdomg  9144  0sdomgOLD  9145  frind  9790  fin23lem26  10365  axdc3lem4  10493  axdc4lem  10495  axcclem  10497  crreczi  14267  ef0lem  16114  lidlnz  21252  nconnsubb  23431  ufileu  23927  itg2cnlem1  25796  plyeq0lem  26249  abelthlem2  26476  ppinprm  27195  chtnprm  27197  sltlpss  27945  mulsval  28135  ltgov  28605  usgr2pthlem  29783  shne0i  31467  pjneli  31742  eleigvec  31976  nmo  32509  qqhval2lem  33982  qqhval2  33983  sibfof  34342  dffr5  35754  ellimits  35911  elicc3  36318  itg2addnclem2  37679  ftc1anclem3  37702  onfrALTlem5  44562  onfrALTlem5VD  44905  limcrecl  45644  dfnbgr6  47843