Theorem necon3bbid 2978

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  necon1abid  2979  necon3bid  2985  eldifsn  4786  php  9247  phpOLD  9259  xmullem2  13307  fzdif1  13645  seqcoll2  14504  cnpart  15279  rlimrecl  15616  ncoprmgcdne1b  16687  prmrp  16749  4sqlem17  16999  mrieqvd  17681  mrieqv2d  17682  pltval  18377  latnlemlt  18517  latnle  18518  odnncl  19563  gexnnod  19606  sylow1lem1  19616  slwpss  19630  lssnle  19692  nzrunit  20524  imadrhmcl  20798  lspsnne1  21119  cnsubrg  21445  psrridm  21983  mhpmulcl  22153  cmpfi  23416  hausdiag  23653  txhaus  23655  isusp  24270  recld2  24836  metdseq0  24876  i1f1lem  25724  aaliou2b  26383  dvloglem  26690  logf1o2  26692  lgsne0  27379  lgsqr  27395  2sqlem7  27468  ostth3  27682  tglngne  28558  tgelrnln  28638  eucrct2eupth  30264  norm1exi  31269  atnemeq0  32396  opeldifid  32612  unitnz  33243  isdrng4  33298  pridln1  33471  mxidln1  33494  ssmxidllem  33501  rprmnz  33548  ply1unit  33600  ply1dg3rt0irred  33607  constrrtll  33772  qtophaus  33835  ordtconnlem1  33923  elzrhunit  33978  sgnneg  34543  subfacp1lem6  35190  maxidln1  38051  smprngopr  38059  lsatnem0  39046  atncmp  39313  atncvrN  39316  cdlema2N  39794  lhpmatb  40033  lhpat3  40048  cdleme3  40239  cdleme7  40251  cdlemg27b  40698  dvh2dimatN  41442  dvh2dim  41447  dochexmidlem1  41462  dochfln0  41479  dvrelog2b  42067  aks6d1c2p2  42120  hashscontpow  42123  rspcsbnea  42132  nna4b4nsq  42670