Theorem pm2.21ddne 3103

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  cshwshashlem2  16432  dprdsn  19160  ablsimpgfind  19234  coseq00topi  25090  tglndim0  26417  ncolncol  26434  footne  26511  s3f1  30625  cycpmco2lem7  30776  linds2eq  30943  sgnsub  31804  sgnmulsgn  31809  sgnmulsgp  31810  pconnconn  32480  osumcllem11N  37104  dochexmidlem8  38605  remul01  39244  fnchoice  41293