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

Theorem pm2.21ddne 2771
 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 2659 . 2
41, 3pm2.21dd 174 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395  =/=wne 2652 This theorem is referenced by:  cshwshashlem2  14581  dprdsn  17083  coseq00topi  22895  tglndim0  24009  ncolncol  24026  footne  24097  sgnsub  28483  sgnmulsgn  28488  sgnmulsgp  28489  pconcon  28676  fnchoice  31404  osumcllem11N  35690  dochexmidlem8  37194 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 185  df-ne 2654
 Copyright terms: Public domain W3C validator