MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3bbid Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 necon3bbid.1 . . . 4 (𝜑 → (𝜓𝐴 = 𝐵))
21bicomd 215 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32necon3abid 3003 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
43bicomd 215 1 (𝜑 → (¬ 𝜓𝐴𝐵))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator