Theorem pm2.21ddne 3030

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

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

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 2945

This theorem is referenced by:  cshwshashlem2  16779  dprdsn  19620  ablsimpgfind  19694  coseq00topi  25640  tglndim0  26971  ncolncol  26988  footne  27065  s3f1  31200  cycpmco2lem7  31378  linds2eq  31554  sgnsub  32490  sgnmulsgn  32495  sgnmulsgp  32496  pconnconn  33172  irrdifflemf  35475  osumcllem11N  37959  dochexmidlem8  39460  sticksstones22  40104  exp11d  40305  remul01  40370  fnchoice  42525