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  4743  php  9135  xmullem2  13184  fzdif1  13525  seqcoll2  14392  cnpart  15167  rlimrecl  15507  ncoprmgcdne1b  16581  prmrp  16643  4sqlem17  16893  mrieqvd  17565  mrieqv2d  17566  pltval  18257  latnlemlt  18399  latnle  18400  odnncl  19478  gexnnod  19521  sylow1lem1  19531  slwpss  19545  lssnle  19607  nzrunit  20461  imadrhmcl  20734  lspsnne1  21076  cnsubrg  21386  psrridm  21922  mhpmulcl  22096  cmpfi  23356  hausdiag  23593  txhaus  23595  isusp  24209  recld2  24763  metdseq0  24803  i1f1lem  25650  aaliou2b  26309  dvloglem  26617  logf1o2  26619  lgsne0  27306  lgsqr  27322  2sqlem7  27395  ostth3  27609  tglngne  28605  tgelrnln  28685  eucrct2eupth  30303  norm1exi  31308  atnemeq0  32435  opeldifid  32656  arginv  32808  sgnneg  32895  unitnz  33302  isdrng4  33358  pridln1  33505  mxidln1  33528  ssmxidllem  33535  rprmnz  33582  ply1unit  33637  ply1dg3rt0irred  33646  constrrtll  33869  qtophaus  33974  ordtconnlem1  34062  elzrhunit  34115  subfacp1lem6  35360  maxidln1  38216  smprngopr  38224  lsatnem0  39342  atncmp  39609  atncvrN  39612  cdlema2N  40089  lhpmatb  40328  lhpat3  40343  cdleme3  40534  cdleme7  40546  cdlemg27b  40993  dvh2dimatN  41737  dvh2dim  41742  dochexmidlem1  41757  dochfln0  41774  dvrelog2b  42357  aks6d1c2p2  42410  hashscontpow  42413  rspcsbnea  42422  nna4b4nsq  42939