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  4230  difsnpss  4771  xpdifid  6141  frpoind  6315  ordintdif  6383  tfi  7829  oelim2  8559  0sdomg  9070  frind  9703  fin23lem26  10278  axdc3lem4  10406  axdc4lem  10408  axcclem  10410  crreczi  14193  ef0lem  16044  lidlnz  21152  nconnsubb  23310  ufileu  23806  itg2cnlem1  25662  plyeq0lem  26115  abelthlem2  26342  ppinprm  27062  chtnprm  27064  sltlpss  27819  mulsval  28012  ltgov  28524  usgr2pthlem  29693  shne0i  31377  pjneli  31652  eleigvec  31886  nmo  32419  qqhval2lem  33971  qqhval2  33972  sibfof  34331  onvf1odlem2  35091  dffr5  35741  ellimits  35898  elicc3  36305  itg2addnclem2  37666  ftc1anclem3  37689  onfrALTlem5  44532  onfrALTlem5VD  44874  limcrecl  45627  dfnbgr6  47857