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  4220  difsnpss  4761  xpdifid  6121  frpoind  6294  ordintdif  6362  tfi  7793  oelim2  8520  0sdomg  9030  frind  9665  fin23lem26  10238  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  crreczi  14153  ef0lem  16003  lidlnz  21167  nconnsubb  23326  ufileu  23822  itg2cnlem1  25678  plyeq0lem  26131  abelthlem2  26358  ppinprm  27078  chtnprm  27080  sltlpss  27840  mulsval  28035  ltgov  28560  usgr2pthlem  29726  shne0i  31410  pjneli  31685  eleigvec  31919  nmo  32452  qqhval2lem  33947  qqhval2  33948  sibfof  34307  onvf1odlem2  35076  dffr5  35726  ellimits  35883  elicc3  36290  itg2addnclem2  37651  ftc1anclem3  37674  onfrALTlem5  44516  onfrALTlem5VD  44858  limcrecl  45611  dfnbgr6  47842