Theorem pm2.21ddne 3040

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  sgnsub  15252  sgnmulsgn  15255  cshwshashlem2  17267  chnub  18789  chnccat  18793  dprdsn  20245  ablsimpgfind  20319  coseq00topi  26824  tglndim0  29090  ncolncol  29108  footne  29191  sgnmulsgp  33416  s3f1  33504  cycpmco2lem7  33686  fracfld  33863  linds2eq  33929  dfufd2lem  34074  ply1dg3rt0irred  34109  ig1pmindeg  34127  esplymhp  34193  pconnconn  35975  irrdifflemf  38226  osumcllem11N  41003  dochexmidlem8  42504  sticksstones22  43198  exp11d  43363  remul01  43438  fnchoice  46015