Theorem necon3bbii 3003

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necon1abii  3004  nssinpss  4219  difsnpss  4766  xpdifid  6150  frpoind  6325  ordintdif  6393  tfi  7829  oelim2  8560  0sdomg  9074  frind  9705  fin23lem26  10279  axdc3lem4  10407  axdc4lem  10409  axcclem  10411  crreczi  14238  ef0lem  16091  lidlnz  21292  nconnsubb  23463  ufileu  23959  itg2cnlem1  25803  plyeq0lem  26250  abelthlem2  26472  ppinprm  27193  chtnprm  27195  ltslpss  27978  mulsval  28179  ltgov  28743  usgr2pthlem  29909  shne0i  31597  pjneli  31872  eleigvec  32106  nmo  32637  qqhval2lem  34239  qqhval2  34240  sibfof  34598  onvf1odlem2  35411  dffr5  36068  ellimits  36222  elicc3  36641  itg2addnclem2  38135  ftc1anclem3  38158  onfrALTlem5  45082  onfrALTlem5VD  45424  limcrecl  46169  dfnbgr6  48443