Theorem necon3bbid 2969

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

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

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 2933

This theorem is referenced by:  necon1abid  2970  necon3bid  2976  eldifsn  4762  php  9221  phpOLD  9231  xmullem2  13281  fzdif1  13622  seqcoll2  14483  cnpart  15259  rlimrecl  15596  ncoprmgcdne1b  16669  prmrp  16731  4sqlem17  16981  mrieqvd  17650  mrieqv2d  17651  pltval  18342  latnlemlt  18482  latnle  18483  odnncl  19526  gexnnod  19569  sylow1lem1  19579  slwpss  19593  lssnle  19655  nzrunit  20484  imadrhmcl  20757  lspsnne1  21078  cnsubrg  21395  psrridm  21923  mhpmulcl  22087  cmpfi  23346  hausdiag  23583  txhaus  23585  isusp  24200  recld2  24754  metdseq0  24794  i1f1lem  25642  aaliou2b  26301  dvloglem  26609  logf1o2  26611  lgsne0  27298  lgsqr  27314  2sqlem7  27387  ostth3  27601  tglngne  28529  tgelrnln  28609  eucrct2eupth  30226  norm1exi  31231  atnemeq0  32358  opeldifid  32580  arginv  32725  sgnneg  32812  unitnz  33234  isdrng4  33289  pridln1  33458  mxidln1  33481  ssmxidllem  33488  rprmnz  33535  ply1unit  33588  ply1dg3rt0irred  33595  constrrtll  33765  qtophaus  33867  ordtconnlem1  33955  elzrhunit  34008  subfacp1lem6  35207  maxidln1  38068  smprngopr  38076  lsatnem0  39063  atncmp  39330  atncvrN  39333  cdlema2N  39811  lhpmatb  40050  lhpat3  40065  cdleme3  40256  cdleme7  40268  cdlemg27b  40715  dvh2dimatN  41459  dvh2dim  41464  dochexmidlem1  41479  dochfln0  41496  dvrelog2b  42079  aks6d1c2p2  42132  hashscontpow  42135  rspcsbnea  42144  nna4b4nsq  42683