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

Theorem necon3bbid 2819
 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 212 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32necon3abid 2818 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
43bicomd 212 1 (𝜑 → (¬ 𝜓𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  necon1abid  2820  necon3bid  2826  eldifsn  4260  php  8029  xmullem2  11967  seqcoll2  13106  cnpart  13828  rlimrecl  14159  ncoprmgcdne1b  15201  prmrp  15262  4sqlem17  15503  mrieqvd  16121  mrieqv2d  16122  pltval  16783  latnlemlt  16907  latnle  16908  odnncl  17787  gexnnod  17826  sylow1lem1  17836  slwpss  17850  lssnle  17910  lspsnne1  18938  nzrunit  19088  psrridm  19225  cnsubrg  19625  cmpfi  21021  hausdiag  21258  txhaus  21260  isusp  21875  recld2  22425  metdseq0  22465  i1f1lem  23262  aaliou2b  23900  dvloglem  24194  logf1o2  24196  lgsne0  24860  lgsqr  24876  2sqlem7  24949  ostth3  25127  tglngne  25245  tgelrnln  25325  norm1exi  27491  atnemeq0  28620  opeldifid  28794  qtophaus  29231  ordtconlem1  29298  elzrhunit  29351  sgnneg  29929  subfacp1lem6  30421  maxidln1  33013  smprngopr  33021  lsatnem0  33350  atncmp  33617  atncvrN  33620  cdlema2N  34096  lhpmatb  34335  lhpat3  34350  cdleme3  34542  cdleme7  34554  cdlemg27b  35002  dvh2dimatN  35747  dvh2dim  35752  dochexmidlem1  35767  dochfln0  35784  eucrct2eupth  41413
 Copyright terms: Public domain W3C validator