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 195 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  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 207  df-ne 2940
This theorem is referenced by:  cshwshashlem2  17135  dprdsn  20057  ablsimpgfind  20131  coseq00topi  26545  tglndim0  28638  ncolncol  28655  footne  28732  s3f1  32932  chnub  33003  cycpmco2lem7  33153  fracfld  33311  linds2eq  33410  dfufd2lem  33578  ply1dg3rt0irred  33608  ig1pmindeg  33623  sgnsub  34548  sgnmulsgn  34553  sgnmulsgp  34554  pconnconn  35237  irrdifflemf  37327  osumcllem11N  39969  dochexmidlem8  41470  sticksstones22  42170  exp11d  42366  remul01  42442  fnchoice  45039
  Copyright terms: Public domain W3C validator