Theorem necon3bbid 2978

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

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

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 2941

This theorem is referenced by:  necon1abid  2979  necon3bid  2985  eldifsn  4790  php  9212  phpOLD  9224  xmullem2  13246  seqcoll2  14428  cnpart  15189  rlimrecl  15526  ncoprmgcdne1b  16589  prmrp  16651  4sqlem17  16896  mrieqvd  17584  mrieqv2d  17585  pltval  18287  latnlemlt  18427  latnle  18428  odnncl  19415  gexnnod  19458  sylow1lem1  19468  slwpss  19482  lssnle  19544  nzrunit  20305  imadrhmcl  20417  lspsnne1  20736  cnsubrg  21011  psrridm  21530  mhpmulcl  21698  cmpfi  22919  hausdiag  23156  txhaus  23158  isusp  23773  recld2  24337  metdseq0  24377  i1f1lem  25213  aaliou2b  25861  dvloglem  26163  logf1o2  26165  lgsne0  26845  lgsqr  26861  2sqlem7  26934  ostth3  27148  tglngne  27839  tgelrnln  27919  eucrct2eupth  29536  norm1exi  30541  atnemeq0  31668  opeldifid  31868  isdrng4  32436  pridln1  32606  mxidln1  32627  ssmxidllem  32634  qtophaus  32885  ordtconnlem1  32973  elzrhunit  33028  sgnneg  33608  subfacp1lem6  34245  maxidln1  37004  smprngopr  37012  lsatnem0  38007  atncmp  38274  atncvrN  38277  cdlema2N  38755  lhpmatb  38994  lhpat3  39009  cdleme3  39200  cdleme7  39212  cdlemg27b  39659  dvh2dimatN  40403  dvh2dim  40408  dochexmidlem1  40423  dochfln0  40440  dvrelog2b  41023  aks6d1c2p2  41049  nna4b4nsq  41490