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 3027
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 2946 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
41, 3pm2.21dd 198 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wne 2941
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 210  df-ne 2942
This theorem is referenced by:  cshwshashlem2  16674  dprdsn  19447  ablsimpgfind  19521  coseq00topi  25416  tglndim0  26744  ncolncol  26761  footne  26838  s3f1  30965  cycpmco2lem7  31142  linds2eq  31313  sgnsub  32247  sgnmulsgn  32252  sgnmulsgp  32253  pconnconn  32929  irrdifflemf  35256  osumcllem11N  37743  dochexmidlem8  39244  sticksstones22  39875  exp11d  40061  remul01  40126  fnchoice  42273
  Copyright terms: Public domain W3C validator