Theorem necon3bbii 3006

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

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

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 2960

This theorem is used by:  necon1abii  3007  nssinpss  4215  difsnpss  4770  xpdifid  6172  frpoind  6366  ordintdif  6435  tfi  7891  oelim2  8635  0sdomg  9156  frind  9784  fin23lem26  10433  axdc3lem4  10561  axdc4lem  10563  axcclem  10565  crreczi  14402  ef0lem  16276  lidlnz  21563  nconnsubb  23774  ufileu  24271  itg2cnlem1  26115  plyeq0lem  26562  abelthlem2  26792  ppinprm  27512  chtnprm  27514  ltslpss  28327  mulsval  28528  ltgov  29093  usgr2pthlem  30382  shne0i  32083  pjneli  32358  eleigvec  32592  nmo  33161  qqhval2lem  34696  qqhval2  34697  sibfof  35055  onvf1odlem2  36045  ellimits  36863  elicc3  37296  itg2addnclem2  38795  ftc1anclem3  38818  onfrALTlem5  45727  onfrALTlem5VD  46069  limcrecl  46856  dfnbgr6  49170