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

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