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

Theorem necon3bbid 3053
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 224 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32necon3abid 3052 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
43bicomd 224 1 (𝜑 → (¬ 𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon1abid  3054  necon3bid  3060  eldifsn  4713  php  8690  xmullem2  12648  seqcoll2  13813  cnpart  14589  rlimrecl  14927  ncoprmgcdne1b  15984  prmrp  16046  4sqlem17  16287  mrieqvd  16899  mrieqv2d  16900  pltval  17560  latnlemlt  17684  latnle  17685  odnncl  18604  gexnnod  18644  sylow1lem1  18654  slwpss  18668  lssnle  18731  lspsnne1  19820  nzrunit  19970  psrridm  20114  cnsubrg  20535  cmpfi  21946  hausdiag  22183  txhaus  22185  isusp  22799  recld2  23351  metdseq0  23391  i1f1lem  24219  aaliou2b  24859  dvloglem  25158  logf1o2  25160  lgsne0  25839  lgsqr  25855  2sqlem7  25928  ostth3  26142  tglngne  26264  tgelrnln  26344  eucrct2eupth  27952  norm1exi  28955  atnemeq0  30082  opeldifid  30278  qtophaus  31000  ordtconnlem1  31067  elzrhunit  31120  sgnneg  31698  subfacp1lem6  32330  maxidln1  35205  smprngopr  35213  lsatnem0  36063  atncmp  36330  atncvrN  36333  cdlema2N  36810  lhpmatb  37049  lhpat3  37064  cdleme3  37255  cdleme7  37267  cdlemg27b  37714  dvh2dimatN  38458  dvh2dim  38463  dochexmidlem1  38478  dochfln0  38495
  Copyright terms: Public domain W3C validator