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

Theorem pm2.21ddne 3101
Description: A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
Hypotheses
Ref Expression
pm2.21ddne.1 (𝜑𝐴 = 𝐵)
pm2.21ddne.2 (𝜑𝐴𝐵)
Assertion
Ref Expression
pm2.21ddne (𝜑𝜓)

Proof of Theorem pm2.21ddne
StepHypRef Expression
1 pm2.21ddne.1 . 2 (𝜑𝐴 = 𝐵)
2 pm2.21ddne.2 . . 3 (𝜑𝐴𝐵)
32neneqd 3021 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
41, 3pm2.21dd 196 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = 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:  cshwshashlem2  16420  dprdsn  19089  ablsimpgfind  19163  coseq00topi  25017  tglndim0  26343  ncolncol  26360  footne  26437  s3f1  30551  cycpmco2lem7  30702  linds2eq  30869  sgnsub  31702  sgnmulsgn  31707  sgnmulsgp  31708  pconnconn  32376  osumcllem11N  36984  dochexmidlem8  38485  remul01  39117  fnchoice  41166
  Copyright terms: Public domain W3C validator