Theorem necon3bbid 2818

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 194   = wceq 1474   ≠ wne 2779

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 195  df-ne 2781

This theorem is referenced by:  necon1abid  2819  necon3bid  2825  eldifsn  4259  php  8006  xmullem2  11924  seqcoll2  13058  cnpart  13774  rlimrecl  14105  ncoprmgcdne1b  15147  prmrp  15208  4sqlem17  15449  mrieqvd  16067  mrieqv2d  16068  pltval  16729  latnlemlt  16853  latnle  16854  odnncl  17733  gexnnod  17772  sylow1lem1  17782  slwpss  17796  lssnle  17856  lspsnne1  18884  nzrunit  19034  psrridm  19171  cnsubrg  19571  cmpfi  20963  hausdiag  21200  txhaus  21202  isusp  21817  recld2  22357  metdseq0  22396  i1f1lem  23179  aaliou2b  23817  dvloglem  24111  logf1o2  24113  lgsne0  24777  lgsqr  24793  2sqlem7  24866  ostth3  25044  tglngne  25163  tgelrnln  25243  norm1exi  27297  atnemeq0  28426  opeldifid  28600  qtophaus  29037  ordtconlem1  29104  elzrhunit  29157  sgnneg  29735  subfacp1lem6  30227  maxidln1  32809  smprngopr  32817  lsatnem0  33146  atncmp  33413  atncvrN  33416  cdlema2N  33892  lhpmatb  34131  lhpat3  34146  cdleme3  34338  cdleme7  34350  cdlemg27b  34798  dvh2dimatN  35543  dvh2dim  35548  dochexmidlem1  35563  dochfln0  35580  eucrct2eupth  41408