Theorem necon3bbid 3004

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   = wceq 1507   ≠ wne 2967

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 199  df-ne 2968

This theorem is referenced by:  necon1abid  3005  necon3bid  3011  eldifsn  4593  php  8497  xmullem2  12474  seqcoll2  13636  cnpart  14460  rlimrecl  14798  ncoprmgcdne1b  15850  prmrp  15912  4sqlem17  16153  mrieqvd  16767  mrieqv2d  16768  pltval  17428  latnlemlt  17552  latnle  17553  odnncl  18435  gexnnod  18474  sylow1lem1  18484  slwpss  18498  lssnle  18558  lspsnne1  19611  nzrunit  19761  psrridm  19898  cnsubrg  20307  cmpfi  21720  hausdiag  21957  txhaus  21959  isusp  22573  recld2  23125  metdseq0  23165  i1f1lem  23993  aaliou2b  24633  dvloglem  24932  logf1o2  24934  lgsne0  25613  lgsqr  25629  2sqlem7  25702  ostth3  25916  tglngne  26038  tgelrnln  26118  eucrct2eupthOLD  27776  eucrct2eupth  27777  norm1exi  28806  atnemeq0  29935  opeldifid  30115  qtophaus  30750  ordtconnlem1  30817  elzrhunit  30870  sgnneg  31450  subfacp1lem6  32023  maxidln1  34770  smprngopr  34778  lsatnem0  35632  atncmp  35899  atncvrN  35902  cdlema2N  36379  lhpmatb  36618  lhpat3  36633  cdleme3  36824  cdleme7  36836  cdlemg27b  37283  dvh2dimatN  38027  dvh2dim  38032  dochexmidlem1  38047  dochfln0  38064