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 1541   ≠ 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  4214  difsnpss  4765  xpdifid  6118  frpoind  6294  wfiOLD  6303  ordintdif  6365  tfi  7785  oelim2  8538  0sdomg  9044  0sdomgOLD  9045  frind  9682  fin23lem26  10257  axdc3lem4  10385  axdc4lem  10387  axcclem  10389  crreczi  14123  ef0lem  15953  lidlnz  20683  nconnsubb  22758  ufileu  23254  itg2cnlem1  25110  plyeq0lem  25555  abelthlem2  25775  ppinprm  26485  chtnprm  26487  sltlpss  27220  ltgov  27425  usgr2pthlem  28597  shne0i  30276  pjneli  30551  eleigvec  30785  nmo  31304  qqhval2lem  32431  qqhval2  32432  sibfof  32809  dffr5  34197  mulsval  34375  ellimits  34462  elicc3  34756  itg2addnclem2  36097  ftc1anclem3  36120  onfrALTlem5  42766  onfrALTlem5VD  43109  limcrecl  43802