Theorem pm2.21ddne 3071

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

Syntax hints:   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  cshwshashlem2  16422  dprdsn  19151  ablsimpgfind  19225  coseq00topi  25095  tglndim0  26423  ncolncol  26440  footne  26517  s3f1  30649  cycpmco2lem7  30824  linds2eq  30995  sgnsub  31912  sgnmulsgn  31917  sgnmulsgp  31918  pconnconn  32591  irrdifflemf  34739  osumcllem11N  37262  dochexmidlem8  38763  remul01  39545  fnchoice  41658