Theorem necon3bbid 2997

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

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

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 2961

This theorem is referenced by:  necon1abid  2998  necon3bid  3004  eldifsn  4749  php  9179  xmullem2  13282  fzdif1  13624  seqcoll2  14492  sgnneg  15127  cnpart  15281  rlimrecl  15621  ncoprmgcdne1b  16698  prmrp  16761  4sqlem17  17011  mrieqvd  17684  mrieqv2d  17685  pltval  18376  latnlemlt  18518  latnle  18519  odnncl  19606  gexnnod  19649  sylow1lem1  19659  slwpss  19673  lssnle  19735  nzrunit  20599  imadrhmcl  20869  lspsnne1  21210  pridln1  21430  cnsubrg  21537  psrridm  22072  mhpmulcl  22272  cmpfi  23526  hausdiag  23763  txhaus  23765  isusp  24379  recld2  24933  metdseq0  24973  i1f1lem  25809  aaliou2b  26463  dvloglem  26771  logf1o2  26773  lgsne0  27457  lgsqr  27473  2sqlem7  27546  ostth3  27760  tglngne  28777  tgelrnln  28857  eucrct2eupth  30505  norm1exi  31511  atnemeq0  32638  opeldifid  32854  arginv  33004  unitnz  33471  isdrng4  33531  mxidln1  33666  ssmxidllem  33673  rprmnz  33727  ply1unit  33782  ply1dg3rt0irred  33791  constrrtll  34038  qtophaus  34143  ordtconnlem1  34231  elzrhunit  34284  subfacp1lem6  35548  maxidln1  38555  smprngopr  38563  lsatnem0  39681  atncmp  39948  atncvrN  39951  cdlema2N  40428  lhpmatb  40667  lhpat3  40682  cdleme3  40873  cdleme7  40885  cdlemg27b  41332  dvh2dimatN  42076  dvh2dim  42081  dochexmidlem1  42096  dochfln0  42113  dvrelog2b  42695  aks6d1c2p2  42748  hashscontpow  42751  rspcsbnea  42760  nna4b4nsq  43254