Theorem pm2.21ddne 3017

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  cshwshashlem2  17121  dprdsn  20024  ablsimpgfind  20098  coseq00topi  26468  tglndim0  28613  ncolncol  28630  footne  28707  sgnsub  32821  sgnmulsgn  32826  sgnmulsgp  32827  s3f1  32927  chnub  32997  cycpmco2lem7  33148  fracfld  33307  linds2eq  33401  dfufd2lem  33569  ply1dg3rt0irred  33600  ig1pmindeg  33616  pconnconn  35258  irrdifflemf  37348  osumcllem11N  39990  dochexmidlem8  41491  sticksstones22  42186  exp11d  42342  remul01  42417  fnchoice  45020