Theorem necon3bbid 2967

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

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

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 2931

This theorem is referenced by:  necon1abid  2968  necon3bid  2974  eldifsn  4739  php  9126  xmullem2  13174  fzdif1  13515  seqcoll2  14382  cnpart  15157  rlimrecl  15497  ncoprmgcdne1b  16571  prmrp  16633  4sqlem17  16883  mrieqvd  17554  mrieqv2d  17555  pltval  18246  latnlemlt  18388  latnle  18389  odnncl  19467  gexnnod  19510  sylow1lem1  19520  slwpss  19534  lssnle  19596  nzrunit  20449  imadrhmcl  20722  lspsnne1  21064  cnsubrg  21374  psrridm  21910  mhpmulcl  22074  cmpfi  23333  hausdiag  23570  txhaus  23572  isusp  24186  recld2  24740  metdseq0  24780  i1f1lem  25627  aaliou2b  26286  dvloglem  26594  logf1o2  26596  lgsne0  27283  lgsqr  27299  2sqlem7  27372  ostth3  27586  tglngne  28538  tgelrnln  28618  eucrct2eupth  30236  norm1exi  31241  atnemeq0  32368  opeldifid  32590  arginv  32742  sgnneg  32827  unitnz  33217  isdrng4  33272  pridln1  33419  mxidln1  33442  ssmxidllem  33449  rprmnz  33496  ply1unit  33549  ply1dg3rt0irred  33557  constrrtll  33755  qtophaus  33860  ordtconnlem1  33948  elzrhunit  34001  subfacp1lem6  35240  maxidln1  38094  smprngopr  38102  lsatnem0  39154  atncmp  39421  atncvrN  39424  cdlema2N  39901  lhpmatb  40140  lhpat3  40155  cdleme3  40346  cdleme7  40358  cdlemg27b  40805  dvh2dimatN  41549  dvh2dim  41554  dochexmidlem1  41569  dochfln0  41586  dvrelog2b  42169  aks6d1c2p2  42222  hashscontpow  42225  rspcsbnea  42234  nna4b4nsq  42768