Theorem necon3bbii 2972

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

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

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 2926

This theorem is referenced by:  necon1abii  2973  nssinpss  4218  difsnpss  4758  xpdifid  6117  frpoind  6290  ordintdif  6358  tfi  7786  oelim2  8513  0sdomg  9023  frind  9646  fin23lem26  10219  axdc3lem4  10347  axdc4lem  10349  axcclem  10351  crreczi  14135  ef0lem  15985  lidlnz  21149  nconnsubb  23308  ufileu  23804  itg2cnlem1  25660  plyeq0lem  26113  abelthlem2  26340  ppinprm  27060  chtnprm  27062  sltlpss  27822  mulsval  28017  ltgov  28542  usgr2pthlem  29708  shne0i  31392  pjneli  31667  eleigvec  31901  nmo  32434  qqhval2lem  33954  qqhval2  33955  sibfof  34314  onvf1odlem2  35087  dffr5  35737  ellimits  35894  elicc3  36301  itg2addnclem2  37662  ftc1anclem3  37685  onfrALTlem5  44526  onfrALTlem5VD  44868  limcrecl  45620  dfnbgr6  47851