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  17067  dprdsn  19968  ablsimpgfind  20042  coseq00topi  26411  tglndim0  28556  ncolncol  28573  footne  28650  sgnsub  32762  sgnmulsgn  32767  sgnmulsgp  32768  s3f1  32868  chnub  32938  cycpmco2lem7  33089  fracfld  33258  linds2eq  33352  dfufd2lem  33520  ply1dg3rt0irred  33551  ig1pmindeg  33567  pconnconn  35218  irrdifflemf  37313  osumcllem11N  39960  dochexmidlem8  41461  sticksstones22  42156  exp11d  42314  remul01  42395  fnchoice  45023