Theorem necon3bbii 2982

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1543   ≠ wne 2935

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 210  df-ne 2936

This theorem is referenced by:  necon1abii  2983  nssinpss  4161  difsnpss  4710  xpdifid  6020  frpoind  6185  wfi  6192  ordintdif  6251  tfi  7621  oelim2  8312  0sdomg  8764  frind  9355  fin23lem26  9922  axdc3lem4  10050  axdc4lem  10052  axcclem  10054  crreczi  13778  ef0lem  15621  lidlnz  20238  nconnsubb  22292  ufileu  22788  itg2cnlem1  24631  plyeq0lem  25076  abelthlem2  25296  ppinprm  26006  chtnprm  26008  ltgov  26660  usgr2pthlem  27822  shne0i  29501  pjneli  29776  eleigvec  30010  nmo  30529  qqhval2lem  31615  qqhval2  31616  sibfof  31991  dffr5  33408  sltlpss  33781  ellimits  33906  elicc3  34200  itg2addnclem2  35523  ftc1anclem3  35546  onfrALTlem5  41787  onfrALTlem5VD  42130  limcrecl  42799