Theorem necon3bbid 2984

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

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

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 2947

This theorem is referenced by:  necon1abid  2985  necon3bid  2991  eldifsn  4811  php  9273  phpOLD  9285  xmullem2  13327  seqcoll2  14514  cnpart  15289  rlimrecl  15626  ncoprmgcdne1b  16697  prmrp  16759  4sqlem17  17008  mrieqvd  17696  mrieqv2d  17697  pltval  18402  latnlemlt  18542  latnle  18543  odnncl  19587  gexnnod  19630  sylow1lem1  19640  slwpss  19654  lssnle  19716  nzrunit  20550  imadrhmcl  20820  lspsnne1  21142  cnsubrg  21468  psrridm  22006  mhpmulcl  22176  cmpfi  23437  hausdiag  23674  txhaus  23676  isusp  24291  recld2  24855  metdseq0  24895  i1f1lem  25743  aaliou2b  26401  dvloglem  26708  logf1o2  26710  lgsne0  27397  lgsqr  27413  2sqlem7  27486  ostth3  27700  tglngne  28576  tgelrnln  28656  eucrct2eupth  30277  norm1exi  31282  atnemeq0  32409  opeldifid  32621  unitnz  33219  isdrng4  33264  pridln1  33436  mxidln1  33459  ssmxidllem  33466  rprmnz  33513  ply1unit  33565  ply1dg3rt0irred  33572  constrrtll  33722  qtophaus  33782  ordtconnlem1  33870  elzrhunit  33925  sgnneg  34505  subfacp1lem6  35153  maxidln1  38004  smprngopr  38012  lsatnem0  39001  atncmp  39268  atncvrN  39271  cdlema2N  39749  lhpmatb  39988  lhpat3  40003  cdleme3  40194  cdleme7  40206  cdlemg27b  40653  dvh2dimatN  41397  dvh2dim  41402  dochexmidlem1  41417  dochfln0  41434  dvrelog2b  42023  aks6d1c2p2  42076  hashscontpow  42079  rspcsbnea  42088  nna4b4nsq  42615