Theorem pm2.21ddne 3026

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2940

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 206  df-ne 2941

This theorem is referenced by:  cshwshashlem2  17032  dprdsn  19908  ablsimpgfind  19982  coseq00topi  26019  tglndim0  27918  ncolncol  27935  footne  28012  s3f1  32151  cycpmco2lem7  32332  linds2eq  32542  ig1pmindeg  32718  sgnsub  33612  sgnmulsgn  33617  sgnmulsgp  33618  pconnconn  34291  irrdifflemf  36298  osumcllem11N  38929  dochexmidlem8  40430  sticksstones22  41076  exp11d  41304  remul01  41368  fnchoice  43801