Theorem pm2.21ddne 3016

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

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

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 2933

This theorem is referenced by:  cshwshashlem2  17024  chnub  18545  chnccat  18549  dprdsn  19967  ablsimpgfind  20041  coseq00topi  26467  tglndim0  28701  ncolncol  28718  footne  28795  sgnsub  32918  sgnmulsgn  32923  sgnmulsgp  32924  s3f1  33029  cycpmco2lem7  33214  fracfld  33390  linds2eq  33462  dfufd2lem  33630  ply1dg3rt0irred  33665  ig1pmindeg  33683  esplymhp  33726  pconnconn  35425  irrdifflemf  37526  osumcllem11N  40222  dochexmidlem8  41723  sticksstones22  42418  exp11d  42577  remul01  42658  fnchoice  45270