Theorem pm2.21ddne 3021

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

Syntax hints:   → wi 4   = wceq 1534   ≠ wne 2935

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 2936

This theorem is referenced by:  cshwshashlem2  17057  dprdsn  19984  ablsimpgfind  20058  coseq00topi  26424  tglndim0  28420  ncolncol  28437  footne  28514  s3f1  32652  cycpmco2lem7  32831  linds2eq  33036  ig1pmindeg  33204  sgnsub  34100  sgnmulsgn  34105  sgnmulsgp  34106  pconnconn  34777  irrdifflemf  36740  osumcllem11N  39376  dochexmidlem8  40877  sticksstones22  41572  exp11d  41807  remul01  41884  fnchoice  44314