Theorem necon3bbid 2980

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 222	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	necon3abid 2979	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
4	3	bicomd 222	1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2942

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 206  df-ne 2943

This theorem is referenced by:  necon1abid  2981  necon3bid  2987  eldifsn  4717  php  8897  xmullem2  12928  seqcoll2  14107  cnpart  14879  rlimrecl  15217  ncoprmgcdne1b  16283  prmrp  16345  4sqlem17  16590  mrieqvd  17264  mrieqv2d  17265  pltval  17965  latnlemlt  18105  latnle  18106  odnncl  19068  gexnnod  19108  sylow1lem1  19118  slwpss  19132  lssnle  19195  lspsnne1  20294  nzrunit  20451  cnsubrg  20570  psrridm  21083  mhpmulcl  21249  cmpfi  22467  hausdiag  22704  txhaus  22706  isusp  23321  recld2  23883  metdseq0  23923  i1f1lem  24758  aaliou2b  25406  dvloglem  25708  logf1o2  25710  lgsne0  26388  lgsqr  26404  2sqlem7  26477  ostth3  26691  tglngne  26815  tgelrnln  26895  eucrct2eupth  28510  norm1exi  29513  atnemeq0  30640  opeldifid  30839  pridln1  31520  mxidln1  31540  ssmxidllem  31543  qtophaus  31688  ordtconnlem1  31776  elzrhunit  31829  sgnneg  32407  subfacp1lem6  33047  maxidln1  36129  smprngopr  36137  lsatnem0  36986  atncmp  37253  atncvrN  37256  cdlema2N  37733  lhpmatb  37972  lhpat3  37987  cdleme3  38178  cdleme7  38190  cdlemg27b  38637  dvh2dimatN  39381  dvh2dim  39386  dochexmidlem1  39401  dochfln0  39418  dvrelog2b  40002  nna4b4nsq  40413