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 3026
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 2945 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
41, 3pm2.21dd 194 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wne 2940
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 2941
This theorem is referenced by:  cshwshashlem2  16895  dprdsn  19734  ablsimpgfind  19808  coseq00topi  25765  tglndim0  27279  ncolncol  27296  footne  27373  s3f1  31508  cycpmco2lem7  31686  linds2eq  31872  sgnsub  32811  sgnmulsgn  32816  sgnmulsgp  32817  pconnconn  33492  irrdifflemf  35609  osumcllem11N  38242  dochexmidlem8  39743  sticksstones22  40389  exp11d  40593  remul01  40658  fnchoice  42901
  Copyright terms: Public domain W3C validator