Theorem necon3bbid 2981

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

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

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 2944

This theorem is referenced by:  necon1abid  2982  necon3bid  2988  eldifsn  4720  php  8993  phpOLD  9005  xmullem2  12999  seqcoll2  14179  cnpart  14951  rlimrecl  15289  ncoprmgcdne1b  16355  prmrp  16417  4sqlem17  16662  mrieqvd  17347  mrieqv2d  17348  pltval  18050  latnlemlt  18190  latnle  18191  odnncl  19153  gexnnod  19193  sylow1lem1  19203  slwpss  19217  lssnle  19280  lspsnne1  20379  nzrunit  20538  cnsubrg  20658  psrridm  21173  mhpmulcl  21339  cmpfi  22559  hausdiag  22796  txhaus  22798  isusp  23413  recld2  23977  metdseq0  24017  i1f1lem  24853  aaliou2b  25501  dvloglem  25803  logf1o2  25805  lgsne0  26483  lgsqr  26499  2sqlem7  26572  ostth3  26786  tglngne  26911  tgelrnln  26991  eucrct2eupth  28609  norm1exi  29612  atnemeq0  30739  opeldifid  30938  pridln1  31618  mxidln1  31638  ssmxidllem  31641  qtophaus  31786  ordtconnlem1  31874  elzrhunit  31929  sgnneg  32507  subfacp1lem6  33147  maxidln1  36202  smprngopr  36210  lsatnem0  37059  atncmp  37326  atncvrN  37329  cdlema2N  37806  lhpmatb  38045  lhpat3  38060  cdleme3  38251  cdleme7  38263  cdlemg27b  38710  dvh2dimatN  39454  dvh2dim  39459  dochexmidlem1  39474  dochfln0  39491  dvrelog2b  40074  nna4b4nsq  40497