Theorem pm2.21ddne 3016

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

Step	Hyp	Ref	Expression
1		pm2.21ddne.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		pm2.21ddne.2	. . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
3	2	neneqd 2937	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
4	1, 3	pm2.21dd 195	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  cshwshashlem2  17067  chnub  18588  chnccat  18592  dprdsn  20013  ablsimpgfind  20087  coseq00topi  26466  tglndim0  28697  ncolncol  28714  footne  28791  sgnsub  32910  sgnmulsgn  32915  sgnmulsgp  32916  s3f1  33007  cycpmco2lem7  33193  fracfld  33369  linds2eq  33441  dfufd2lem  33609  ply1dg3rt0irred  33644  ig1pmindeg  33662  esplymhp  33712  pconnconn  35413  irrdifflemf  37639  osumcllem11N  40412  dochexmidlem8  41913  sticksstones22  42607  exp11d  42758  remul01  42839  fnchoice  45460