Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21ddne Structured version   Visualization version   GIF version

Theorem pm2.21ddne 2907
 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 2828 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
41, 3pm2.21dd 186 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1523   ≠ wne 2823 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 197  df-ne 2824 This theorem is referenced by:  cshwshashlem2  15850  dprdsn  18481  coseq00topi  24299  tglndim0  25569  ncolncol  25586  footne  25660  sgnsub  30734  sgnmulsgn  30739  sgnmulsgp  30740  pconnconn  31339  osumcllem11N  35570  dochexmidlem8  37073  fnchoice  39502
 Copyright terms: Public domain W3C validator