Theorem necon3bbid 2978

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

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

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 206  df-ne 2941

This theorem is referenced by:  necon1abid  2979  necon3bid  2985  eldifsn  4790  php  9209  phpOLD  9221  xmullem2  13243  seqcoll2  14425  cnpart  15186  rlimrecl  15523  ncoprmgcdne1b  16586  prmrp  16648  4sqlem17  16893  mrieqvd  17581  mrieqv2d  17582  pltval  18284  latnlemlt  18424  latnle  18425  odnncl  19412  gexnnod  19455  sylow1lem1  19465  slwpss  19479  lssnle  19541  nzrunit  20300  imadrhmcl  20412  lspsnne1  20729  cnsubrg  21004  psrridm  21523  mhpmulcl  21691  cmpfi  22911  hausdiag  23148  txhaus  23150  isusp  23765  recld2  24329  metdseq0  24369  i1f1lem  25205  aaliou2b  25853  dvloglem  26155  logf1o2  26157  lgsne0  26835  lgsqr  26851  2sqlem7  26924  ostth3  27138  tglngne  27798  tgelrnln  27878  eucrct2eupth  29495  norm1exi  30498  atnemeq0  31625  opeldifid  31825  isdrng4  32390  pridln1  32556  mxidln1  32577  ssmxidllem  32584  qtophaus  32811  ordtconnlem1  32899  elzrhunit  32954  sgnneg  33534  subfacp1lem6  34171  maxidln1  36907  smprngopr  36915  lsatnem0  37910  atncmp  38177  atncvrN  38180  cdlema2N  38658  lhpmatb  38897  lhpat3  38912  cdleme3  39103  cdleme7  39115  cdlemg27b  39562  dvh2dimatN  40306  dvh2dim  40311  dochexmidlem1  40326  dochfln0  40343  dvrelog2b  40926  aks6d1c2p2  40952  nna4b4nsq  41403