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  4732  php  9141  xmullem2  13217  fzdif1  13559  seqcoll2  14427  cnpart  15202  rlimrecl  15542  ncoprmgcdne1b  16619  prmrp  16682  4sqlem17  16932  mrieqvd  17604  mrieqv2d  17605  pltval  18296  latnlemlt  18438  latnle  18439  odnncl  19520  gexnnod  19563  sylow1lem1  19573  slwpss  19587  lssnle  19649  nzrunit  20501  imadrhmcl  20774  lspsnne1  21115  cnsubrg  21407  psrridm  21941  mhpmulcl  22115  cmpfi  23373  hausdiag  23610  txhaus  23612  isusp  24226  recld2  24780  metdseq0  24820  i1f1lem  25656  aaliou2b  26307  dvloglem  26612  logf1o2  26614  lgsne0  27298  lgsqr  27314  2sqlem7  27387  ostth3  27601  tglngne  28618  tgelrnln  28698  eucrct2eupth  30315  norm1exi  31321  atnemeq0  32448  opeldifid  32669  arginv  32820  sgnneg  32906  unitnz  33300  isdrng4  33356  pridln1  33503  mxidln1  33526  ssmxidllem  33533  rprmnz  33580  ply1unit  33635  ply1dg3rt0irred  33644  constrrtll  33875  qtophaus  33980  ordtconnlem1  34068  elzrhunit  34121  subfacp1lem6  35367  maxidln1  38365  smprngopr  38373  lsatnem0  39491  atncmp  39758  atncvrN  39761  cdlema2N  40238  lhpmatb  40477  lhpat3  40492  cdleme3  40683  cdleme7  40695  cdlemg27b  41142  dvh2dimatN  41886  dvh2dim  41891  dochexmidlem1  41906  dochfln0  41923  dvrelog2b  42505  aks6d1c2p2  42558  hashscontpow  42561  rspcsbnea  42570  nna4b4nsq  43093