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 3024
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 2943 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
41, 3pm2.21dd 195 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wne 2938
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 207  df-ne 2939
This theorem is referenced by:  cshwshashlem2  17131  dprdsn  20071  ablsimpgfind  20145  coseq00topi  26559  tglndim0  28652  ncolncol  28669  footne  28746  s3f1  32916  chnub  32986  cycpmco2lem7  33135  fracfld  33290  linds2eq  33389  dfufd2lem  33557  ply1dg3rt0irred  33587  ig1pmindeg  33602  sgnsub  34526  sgnmulsgn  34531  sgnmulsgp  34532  pconnconn  35216  irrdifflemf  37308  osumcllem11N  39949  dochexmidlem8  41450  sticksstones22  42150  exp11d  42340  remul01  42414  fnchoice  44967
  Copyright terms: Public domain W3C validator