Theorem necon3bbid 2963

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

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

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 2927

This theorem is referenced by:  necon1abid  2964  necon3bid  2970  eldifsn  4753  php  9177  xmullem2  13232  fzdif1  13573  seqcoll2  14437  cnpart  15213  rlimrecl  15553  ncoprmgcdne1b  16627  prmrp  16689  4sqlem17  16939  mrieqvd  17606  mrieqv2d  17607  pltval  18298  latnlemlt  18438  latnle  18439  odnncl  19482  gexnnod  19525  sylow1lem1  19535  slwpss  19549  lssnle  19611  nzrunit  20440  imadrhmcl  20713  lspsnne1  21034  cnsubrg  21351  psrridm  21879  mhpmulcl  22043  cmpfi  23302  hausdiag  23539  txhaus  23541  isusp  24156  recld2  24710  metdseq0  24750  i1f1lem  25597  aaliou2b  26256  dvloglem  26564  logf1o2  26566  lgsne0  27253  lgsqr  27269  2sqlem7  27342  ostth3  27556  tglngne  28484  tgelrnln  28564  eucrct2eupth  30181  norm1exi  31186  atnemeq0  32313  opeldifid  32535  arginv  32678  sgnneg  32765  unitnz  33197  isdrng4  33252  pridln1  33421  mxidln1  33444  ssmxidllem  33451  rprmnz  33498  ply1unit  33551  ply1dg3rt0irred  33558  constrrtll  33728  qtophaus  33833  ordtconnlem1  33921  elzrhunit  33974  subfacp1lem6  35179  maxidln1  38045  smprngopr  38053  lsatnem0  39045  atncmp  39312  atncvrN  39315  cdlema2N  39793  lhpmatb  40032  lhpat3  40047  cdleme3  40238  cdleme7  40250  cdlemg27b  40697  dvh2dimatN  41441  dvh2dim  41446  dochexmidlem1  41461  dochfln0  41478  dvrelog2b  42061  aks6d1c2p2  42114  hashscontpow  42117  rspcsbnea  42126  nna4b4nsq  42655