Theorem pm2.21ddne 3009

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 2930	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
4	1, 3	pm2.21dd 195	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  cshwshashlem2  17026  dprdsn  19935  ablsimpgfind  20009  coseq00topi  26427  tglndim0  28592  ncolncol  28609  footne  28686  sgnsub  32795  sgnmulsgn  32800  sgnmulsgp  32801  s3f1  32901  chnub  32967  cycpmco2lem7  33087  fracfld  33257  linds2eq  33328  dfufd2lem  33496  ply1dg3rt0irred  33527  ig1pmindeg  33543  pconnconn  35203  irrdifflemf  37298  osumcllem11N  39945  dochexmidlem8  41446  sticksstones22  42141  exp11d  42299  remul01  42380  fnchoice  45007