Theorem necon3bbid 2972

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

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

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 2936

This theorem is referenced by:  necon1abid  2973  necon3bid  2979  eldifsn  4690  php  8819  xmullem2  12838  seqcoll2  14014  cnpart  14786  rlimrecl  15124  ncoprmgcdne1b  16188  prmrp  16250  4sqlem17  16495  mrieqvd  17113  mrieqv2d  17114  pltval  17810  latnlemlt  17950  latnle  17951  odnncl  18909  gexnnod  18949  sylow1lem1  18959  slwpss  18973  lssnle  19036  lspsnne1  20126  nzrunit  20277  cnsubrg  20395  psrridm  20901  mhpmulcl  21061  cmpfi  22277  hausdiag  22514  txhaus  22516  isusp  23131  recld2  23683  metdseq0  23723  i1f1lem  24558  aaliou2b  25206  dvloglem  25508  logf1o2  25510  lgsne0  26188  lgsqr  26204  2sqlem7  26277  ostth3  26491  tglngne  26613  tgelrnln  26693  eucrct2eupth  28300  norm1exi  29303  atnemeq0  30430  opeldifid  30629  pridln1  31304  mxidln1  31324  ssmxidllem  31327  qtophaus  31472  ordtconnlem1  31560  elzrhunit  31613  sgnneg  32191  subfacp1lem6  32832  maxidln1  35896  smprngopr  35904  lsatnem0  36753  atncmp  37020  atncvrN  37023  cdlema2N  37500  lhpmatb  37739  lhpat3  37754  cdleme3  37945  cdleme7  37957  cdlemg27b  38404  dvh2dimatN  39148  dvh2dim  39153  dochexmidlem1  39168  dochfln0  39185  dvrelog2b  39764  nna4b4nsq  40152