Theorem necon3bbid 2992

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon1abid  2993  necon3bid  2999  eldifsn  4747  php  9200  xmullem2  13365  fzdif1  13708  seqcoll2  14578  sgnneg  15221  cnpart  15375  rlimrecl  15715  ncoprmgcdne1b  16788  prmrp  16851  4sqlem17  17101  mrieqvd  17774  mrieqv2d  17775  pltval  18466  latnlemlt  18608  latnle  18609  degenmgm2nfun  19101  odnncl  19721  gexnnod  19764  sylow1lem1  19774  slwpss  19788  lssnle  19850  nzrunit  20737  isdrng4  20954  imadrhmcl  21016  lspsnne1  21357  pridln1  21586  cnsubrg  21695  psrridm  22232  mhpmulcl  22432  cmpfi  23688  hausdiag  23926  txhaus  23928  isusp  24542  recld2  25096  metdseq0  25136  i1f1lem  25972  aaliou2b  26632  dvloglem  26940  logf1o2  26942  lgsne0  27626  lgsqr  27642  2sqlem7  27715  ostth3  27929  tglngne  28947  tgelrnln  29032  eucrct2eupth  30780  norm1exi  31786  atnemeq0  32913  opeldifid  33127  arginv  33273  unitnz  33733  mxidln1  33925  ssmxidllem  33932  rprmnz  33986  ply1unit  34041  ply1dg3rt0irred  34050  constrrtll  34297  qtophaus  34402  ordtconnlem1  34490  elzrhunit  34543  subfacp1lem6  35871  maxidln1  38898  smprngopr  38906  lsatnem0  40022  atncmp  40289  atncvrN  40292  cdlema2N  40769  lhpmatb  41008  lhpat3  41023  cdleme3  41214  cdleme7  41226  cdlemg27b  41673  dvh2dimatN  42417  dvh2dim  42422  dochexmidlem1  42437  dochfln0  42454  dvrelog2b  43036  aks6d1c2p2  43089  hashscontpow  43092  rspcsbnea  43101  nna4b4nsq  43610