Theorem necon3bbid 2993

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1568   ≠ wne 2956

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 210  df-ne 2957

This theorem is referenced by:  necon1abid  2994  necon3bid  3000  eldifsn  4752  php  9190  xmullem2  13290  fzdif1  13633  seqcoll2  14502  sgnneg  15137  cnpart  15291  rlimrecl  15631  ncoprmgcdne1b  16707  prmrp  16770  4sqlem17  17020  mrieqvd  17693  mrieqv2d  17694  pltval  18385  latnlemlt  18527  latnle  18528  odnncl  19614  gexnnod  19657  sylow1lem1  19667  slwpss  19681  lssnle  19743  nzrunit  20607  isdrng4  20824  imadrhmcl  20879  lspsnne1  21220  pridln1  21447  cnsubrg  21556  psrridm  22091  mhpmulcl  22291  cmpfi  23544  hausdiag  23781  txhaus  23783  isusp  24397  recld2  24951  metdseq0  24991  i1f1lem  25827  aaliou2b  26481  dvloglem  26789  logf1o2  26791  lgsne0  27475  lgsqr  27491  2sqlem7  27564  ostth3  27778  tglngne  28795  tgelrnln  28879  eucrct2eupth  30562  norm1exi  31568  atnemeq0  32695  opeldifid  32910  arginv  33058  unitnz  33524  mxidln1  33715  ssmxidllem  33722  rprmnz  33776  ply1unit  33831  ply1dg3rt0irred  33840  constrrtll  34087  qtophaus  34192  ordtconnlem1  34280  elzrhunit  34333  subfacp1lem6  35643  maxidln1  38661  smprngopr  38669  lsatnem0  39787  atncmp  40054  atncvrN  40057  cdlema2N  40534  lhpmatb  40773  lhpat3  40788  cdleme3  40979  cdleme7  40991  cdlemg27b  41438  dvh2dimatN  42182  dvh2dim  42187  dochexmidlem1  42202  dochfln0  42219  dvrelog2b  42801  aks6d1c2p2  42854  hashscontpow  42857  rspcsbnea  42866  nna4b4nsq  43362