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 3098
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 3018 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
41, 3pm2.21dd 196 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3013
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 3014
This theorem is referenced by:  cshwshashlem2  16418  dprdsn  19087  ablsimpgfind  19161  coseq00topi  25015  tglndim0  26342  ncolncol  26359  footne  26436  s3f1  30550  cycpmco2lem7  30701  linds2eq  30868  sgnsub  31701  sgnmulsgn  31706  sgnmulsgp  31707  pconnconn  32375  osumcllem11N  36982  dochexmidlem8  38483  remul01  39115  fnchoice  41163
  Copyright terms: Public domain W3C validator