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 1541   ≠ 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  4736  php  9111  xmullem2  13156  fzdif1  13497  seqcoll2  14364  cnpart  15139  rlimrecl  15479  ncoprmgcdne1b  16553  prmrp  16615  4sqlem17  16865  mrieqvd  17536  mrieqv2d  17537  pltval  18228  latnlemlt  18370  latnle  18371  odnncl  19450  gexnnod  19493  sylow1lem1  19503  slwpss  19517  lssnle  19579  nzrunit  20432  imadrhmcl  20705  lspsnne1  21047  cnsubrg  21357  psrridm  21893  mhpmulcl  22057  cmpfi  23316  hausdiag  23553  txhaus  23555  isusp  24169  recld2  24723  metdseq0  24763  i1f1lem  25610  aaliou2b  26269  dvloglem  26577  logf1o2  26579  lgsne0  27266  lgsqr  27282  2sqlem7  27355  ostth3  27569  tglngne  28521  tgelrnln  28601  eucrct2eupth  30215  norm1exi  31220  atnemeq0  32347  opeldifid  32569  arginv  32721  sgnneg  32806  unitnz  33196  isdrng4  33251  pridln1  33398  mxidln1  33421  ssmxidllem  33428  rprmnz  33475  ply1unit  33528  ply1dg3rt0irred  33536  constrrtll  33734  qtophaus  33839  ordtconnlem1  33927  elzrhunit  33980  subfacp1lem6  35197  maxidln1  38063  smprngopr  38071  lsatnem0  39063  atncmp  39330  atncvrN  39333  cdlema2N  39810  lhpmatb  40049  lhpat3  40064  cdleme3  40255  cdleme7  40267  cdlemg27b  40714  dvh2dimatN  41458  dvh2dim  41463  dochexmidlem1  41478  dochfln0  41495  dvrelog2b  42078  aks6d1c2p2  42131  hashscontpow  42134  rspcsbnea  42143  nna4b4nsq  42672