Theorem pm2.21ddne 3013

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

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

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 2930

This theorem is referenced by:  cshwshashlem2  17010  chnub  18530  chnccat  18534  dprdsn  19952  ablsimpgfind  20026  coseq00topi  26439  tglndim0  28608  ncolncol  28625  footne  28702  sgnsub  32825  sgnmulsgn  32830  sgnmulsgp  32831  s3f1  32935  cycpmco2lem7  33108  fracfld  33281  linds2eq  33353  dfufd2lem  33521  ply1dg3rt0irred  33553  ig1pmindeg  33569  esplymhp  33608  pconnconn  35296  irrdifflemf  37390  osumcllem11N  40085  dochexmidlem8  41586  sticksstones22  42281  exp11d  42444  remul01  42525  fnchoice  45150