Theorem necon3bbii 3008

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2962

This theorem is used by:  necon1abii  3009  nssinpss  4223  difsnpss  4780  xpdifid  6170  frpoind  6350  ordintdif  6419  tfi  7858  oelim2  8590  0sdomg  9104  frind  9732  fin23lem26  10327  axdc3lem4  10455  axdc4lem  10457  axcclem  10459  crreczi  14284  ef0lem  16157  lidlnz  21413  nconnsubb  23617  ufileu  24113  itg2cnlem1  25957  plyeq0lem  26404  abelthlem2  26632  ppinprm  27353  chtnprm  27355  ltslpss  28138  mulsval  28339  ltgov  28903  usgr2pthlem  30149  shne0i  31837  pjneli  32112  eleigvec  32346  nmo  32873  qqhval2lem  34402  qqhval2  34403  sibfof  34762  onvf1odlem2  35612  dffr5  36267  ellimits  36421  elicc3  36869  itg2addnclem2  38364  ftc1anclem3  38387  onfrALTlem5  45292  onfrALTlem5VD  45634  limcrecl  46386  dfnbgr6  48663