Theorem pm2.21ddne 3019

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 196	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   = wceq 1547   ≠ 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 208  df-ne 2936

This theorem is referenced by:  cshwshashlem2  17065  chnub  18586  chnccat  18590  dprdsn  20011  ablsimpgfind  20085  coseq00topi  26491  tglndim0  28722  ncolncol  28739  footne  28816  sgnsub  32936  sgnmulsgn  32941  sgnmulsgp  32942  s3f1  33033  cycpmco2lem7  33220  fracfld  33399  linds2eq  33471  dfufd2lem  33639  ply1dg3rt0irred  33674  ig1pmindeg  33692  esplymhp  33759  pconnconn  35466  irrdifflemf  37692  osumcllem11N  40465  dochexmidlem8  41966  sticksstones22  42660  exp11d  42810  remul01  42891  fnchoice  45484