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  4737  php  9121  xmullem2  13167  fzdif1  13508  seqcoll2  14372  cnpart  15147  rlimrecl  15487  ncoprmgcdne1b  16561  prmrp  16623  4sqlem17  16873  mrieqvd  17544  mrieqv2d  17545  pltval  18236  latnlemlt  18378  latnle  18379  odnncl  19424  gexnnod  19467  sylow1lem1  19477  slwpss  19491  lssnle  19553  nzrunit  20409  imadrhmcl  20682  lspsnne1  21024  cnsubrg  21334  psrridm  21870  mhpmulcl  22034  cmpfi  23293  hausdiag  23530  txhaus  23532  isusp  24147  recld2  24701  metdseq0  24741  i1f1lem  25588  aaliou2b  26247  dvloglem  26555  logf1o2  26557  lgsne0  27244  lgsqr  27260  2sqlem7  27333  ostth3  27547  tglngne  28495  tgelrnln  28575  eucrct2eupth  30189  norm1exi  31194  atnemeq0  32321  opeldifid  32543  arginv  32691  sgnneg  32778  unitnz  33179  isdrng4  33234  pridln1  33380  mxidln1  33403  ssmxidllem  33410  rprmnz  33457  ply1unit  33510  ply1dg3rt0irred  33518  constrrtll  33698  qtophaus  33803  ordtconnlem1  33891  elzrhunit  33944  subfacp1lem6  35162  maxidln1  38028  smprngopr  38036  lsatnem0  39028  atncmp  39295  atncvrN  39298  cdlema2N  39775  lhpmatb  40014  lhpat3  40029  cdleme3  40220  cdleme7  40232  cdlemg27b  40679  dvh2dimatN  41423  dvh2dim  41428  dochexmidlem1  41443  dochfln0  41460  dvrelog2b  42043  aks6d1c2p2  42096  hashscontpow  42099  rspcsbnea  42108  nna4b4nsq  42637