Theorem necon3bbid 2819

Description: Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)

Hypothesis

Ref	Expression
necon3bbid.1	⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))

Assertion

Ref	Expression
necon3bbid	⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))

Proof of Theorem necon3bbid

Step	Hyp	Ref	Expression
1		necon3bbid.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))
2	1	bicomd 212	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	necon3abid 2818	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
4	3	bicomd 212	1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon1abid  2820  necon3bid  2826  eldifsn  4260  php  8029  xmullem2  11967  seqcoll2  13106  cnpart  13828  rlimrecl  14159  ncoprmgcdne1b  15201  prmrp  15262  4sqlem17  15503  mrieqvd  16121  mrieqv2d  16122  pltval  16783  latnlemlt  16907  latnle  16908  odnncl  17787  gexnnod  17826  sylow1lem1  17836  slwpss  17850  lssnle  17910  lspsnne1  18938  nzrunit  19088  psrridm  19225  cnsubrg  19625  cmpfi  21021  hausdiag  21258  txhaus  21260  isusp  21875  recld2  22425  metdseq0  22465  i1f1lem  23262  aaliou2b  23900  dvloglem  24194  logf1o2  24196  lgsne0  24860  lgsqr  24876  2sqlem7  24949  ostth3  25127  tglngne  25245  tgelrnln  25325  norm1exi  27491  atnemeq0  28620  opeldifid  28794  qtophaus  29231  ordtconlem1  29298  elzrhunit  29351  sgnneg  29929  subfacp1lem6  30421  maxidln1  33013  smprngopr  33021  lsatnem0  33350  atncmp  33617  atncvrN  33620  cdlema2N  34096  lhpmatb  34335  lhpat3  34350  cdleme3  34542  cdleme7  34554  cdlemg27b  35002  dvh2dimatN  35747  dvh2dim  35752  dochexmidlem1  35767  dochfln0  35784  eucrct2eupth  41413