Theorem necon3bbid 2979

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

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

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 2942

This theorem is referenced by:  necon1abid  2980  necon3bid  2986  eldifsn  4791  php  9210  phpOLD  9222  xmullem2  13244  seqcoll2  14426  cnpart  15187  rlimrecl  15524  ncoprmgcdne1b  16587  prmrp  16649  4sqlem17  16894  mrieqvd  17582  mrieqv2d  17583  pltval  18285  latnlemlt  18425  latnle  18426  odnncl  19413  gexnnod  19456  sylow1lem1  19466  slwpss  19480  lssnle  19542  nzrunit  20301  imadrhmcl  20413  lspsnne1  20730  cnsubrg  21005  psrridm  21524  mhpmulcl  21692  cmpfi  22912  hausdiag  23149  txhaus  23151  isusp  23766  recld2  24330  metdseq0  24370  i1f1lem  25206  aaliou2b  25854  dvloglem  26156  logf1o2  26158  lgsne0  26838  lgsqr  26854  2sqlem7  26927  ostth3  27141  tglngne  27801  tgelrnln  27881  eucrct2eupth  29498  norm1exi  30503  atnemeq0  31630  opeldifid  31830  isdrng4  32395  pridln1  32561  mxidln1  32582  ssmxidllem  32589  qtophaus  32816  ordtconnlem1  32904  elzrhunit  32959  sgnneg  33539  subfacp1lem6  34176  maxidln1  36912  smprngopr  36920  lsatnem0  37915  atncmp  38182  atncvrN  38185  cdlema2N  38663  lhpmatb  38902  lhpat3  38917  cdleme3  39108  cdleme7  39120  cdlemg27b  39567  dvh2dimatN  40311  dvh2dim  40316  dochexmidlem1  40331  dochfln0  40348  dvrelog2b  40931  aks6d1c2p2  40957  nna4b4nsq  41402