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 3025
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 2944 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
41, 3pm2.21dd 194 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wne 2939
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 206  df-ne 2940
This theorem is referenced by:  cshwshashlem2  17035  dprdsn  19948  ablsimpgfind  20022  coseq00topi  26245  tglndim0  28144  ncolncol  28161  footne  28238  s3f1  32377  cycpmco2lem7  32558  linds2eq  32768  ig1pmindeg  32944  sgnsub  33838  sgnmulsgn  33843  sgnmulsgp  33844  pconnconn  34517  irrdifflemf  36510  osumcllem11N  39141  dochexmidlem8  40642  sticksstones22  41291  exp11d  41519  remul01  41583  fnchoice  44016
  Copyright terms: Public domain W3C validator