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 3105
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 3025 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
41, 3pm2.21dd 196 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wne 3020
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 3021
This theorem is referenced by:  cshwshashlem2  16422  dprdsn  19080  ablsimpgfind  19154  coseq00topi  25005  tglndim0  26331  ncolncol  26348  footne  26425  s3f1  30539  cycpmco2lem7  30690  linds2eq  30857  sgnsub  31690  sgnmulsgn  31695  sgnmulsgp  31696  pconnconn  32364  osumcllem11N  36971  dochexmidlem8  38472  remul01  39104  fnchoice  41153
  Copyright terms: Public domain W3C validator