Theorem necon3bbid 2988

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1554   ≠ wne 2951

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 209  df-ne 2952

This theorem is referenced by:  necon1abid  2989  necon3bid  2995  eldifsn  4740  php  9164  xmullem2  13258  fzdif1  13600  seqcoll2  14468  cnpart  15243  rlimrecl  15583  ncoprmgcdne1b  16660  prmrp  16723  4sqlem17  16973  mrieqvd  17646  mrieqv2d  17647  pltval  18338  latnlemlt  18480  latnle  18481  odnncl  19561  gexnnod  19604  sylow1lem1  19614  slwpss  19628  lssnle  19690  nzrunit  20546  imadrhmcl  20819  lspsnne1  21160  cnsubrg  21452  psrridm  21987  mhpmulcl  22187  cmpfi  23441  hausdiag  23678  txhaus  23680  isusp  24294  recld2  24848  metdseq0  24888  i1f1lem  25724  aaliou2b  26375  dvloglem  26683  logf1o2  26685  lgsne0  27369  lgsqr  27385  2sqlem7  27458  ostth3  27672  tglngne  28689  tgelrnln  28769  eucrct2eupth  30386  norm1exi  31392  atnemeq0  32519  opeldifid  32741  arginv  32892  sgnneg  32978  unitnz  33373  isdrng4  33436  pridln1  33583  mxidln1  33608  ssmxidllem  33615  rprmnz  33670  ply1unit  33725  ply1dg3rt0irred  33734  constrrtll  33982  qtophaus  34087  ordtconnlem1  34175  elzrhunit  34228  subfacp1lem6  35483  maxidln1  38491  smprngopr  38499  lsatnem0  39617  atncmp  39884  atncvrN  39887  cdlema2N  40364  lhpmatb  40603  lhpat3  40618  cdleme3  40809  cdleme7  40821  cdlemg27b  41268  dvh2dimatN  42012  dvh2dim  42017  dochexmidlem1  42032  dochfln0  42049  dvrelog2b  42631  aks6d1c2p2  42684  hashscontpow  42687  rspcsbnea  42696  nna4b4nsq  43190