Theorem necon3bbid 2970

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

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

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 2934

This theorem is referenced by:  necon1abid  2971  necon3bid  2977  eldifsn  4744  php  9143  xmullem2  13192  fzdif1  13533  seqcoll2  14400  cnpart  15175  rlimrecl  15515  ncoprmgcdne1b  16589  prmrp  16651  4sqlem17  16901  mrieqvd  17573  mrieqv2d  17574  pltval  18265  latnlemlt  18407  latnle  18408  odnncl  19486  gexnnod  19529  sylow1lem1  19539  slwpss  19553  lssnle  19615  nzrunit  20469  imadrhmcl  20742  lspsnne1  21084  cnsubrg  21394  psrridm  21930  mhpmulcl  22104  cmpfi  23364  hausdiag  23601  txhaus  23603  isusp  24217  recld2  24771  metdseq0  24811  i1f1lem  25658  aaliou2b  26317  dvloglem  26625  logf1o2  26627  lgsne0  27314  lgsqr  27330  2sqlem7  27403  ostth3  27617  tglngne  28634  tgelrnln  28714  eucrct2eupth  30332  norm1exi  31337  atnemeq0  32464  opeldifid  32685  arginv  32837  sgnneg  32924  unitnz  33332  isdrng4  33388  pridln1  33535  mxidln1  33558  ssmxidllem  33565  rprmnz  33612  ply1unit  33667  ply1dg3rt0irred  33676  constrrtll  33908  qtophaus  34013  ordtconnlem1  34101  elzrhunit  34154  subfacp1lem6  35398  maxidln1  38284  smprngopr  38292  lsatnem0  39410  atncmp  39677  atncvrN  39680  cdlema2N  40157  lhpmatb  40396  lhpat3  40411  cdleme3  40602  cdleme7  40614  cdlemg27b  41061  dvh2dimatN  41805  dvh2dim  41810  dochexmidlem1  41825  dochfln0  41842  dvrelog2b  42425  aks6d1c2p2  42478  hashscontpow  42481  rspcsbnea  42490  nna4b4nsq  43007