Theorem pm2.21ddne 3027

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

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

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 2942

This theorem is referenced by:  cshwshashlem2  17030  dprdsn  19906  ablsimpgfind  19980  coseq00topi  26012  tglndim0  27880  ncolncol  27897  footne  27974  s3f1  32113  cycpmco2lem7  32291  linds2eq  32497  ig1pmindeg  32671  sgnsub  33543  sgnmulsgn  33548  sgnmulsgp  33549  pconnconn  34222  irrdifflemf  36206  osumcllem11N  38837  dochexmidlem8  40338  sticksstones22  40984  exp11d  41216  remul01  41280  fnchoice  43713