Theorem necon3bbid 2962

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

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

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 2926

This theorem is referenced by:  necon1abid  2963  necon3bid  2969  eldifsn  4750  php  9171  xmullem2  13225  fzdif1  13566  seqcoll2  14430  cnpart  15206  rlimrecl  15546  ncoprmgcdne1b  16620  prmrp  16682  4sqlem17  16932  mrieqvd  17599  mrieqv2d  17600  pltval  18291  latnlemlt  18431  latnle  18432  odnncl  19475  gexnnod  19518  sylow1lem1  19528  slwpss  19542  lssnle  19604  nzrunit  20433  imadrhmcl  20706  lspsnne1  21027  cnsubrg  21344  psrridm  21872  mhpmulcl  22036  cmpfi  23295  hausdiag  23532  txhaus  23534  isusp  24149  recld2  24703  metdseq0  24743  i1f1lem  25590  aaliou2b  26249  dvloglem  26557  logf1o2  26559  lgsne0  27246  lgsqr  27262  2sqlem7  27335  ostth3  27549  tglngne  28477  tgelrnln  28557  eucrct2eupth  30174  norm1exi  31179  atnemeq0  32306  opeldifid  32528  arginv  32671  sgnneg  32758  unitnz  33190  isdrng4  33245  pridln1  33414  mxidln1  33437  ssmxidllem  33444  rprmnz  33491  ply1unit  33544  ply1dg3rt0irred  33551  constrrtll  33721  qtophaus  33826  ordtconnlem1  33914  elzrhunit  33967  subfacp1lem6  35172  maxidln1  38038  smprngopr  38046  lsatnem0  39038  atncmp  39305  atncvrN  39308  cdlema2N  39786  lhpmatb  40025  lhpat3  40040  cdleme3  40231  cdleme7  40243  cdlemg27b  40690  dvh2dimatN  41434  dvh2dim  41439  dochexmidlem1  41454  dochfln0  41471  dvrelog2b  42054  aks6d1c2p2  42107  hashscontpow  42110  rspcsbnea  42119  nna4b4nsq  42648