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 1542   ≠ 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  17058  chnub  18579  chnccat  18583  dprdsn  20004  ablsimpgfind  20078  coseq00topi  26479  tglndim0  28711  ncolncol  28728  footne  28805  sgnsub  32925  sgnmulsgn  32930  sgnmulsgp  32931  s3f1  33022  cycpmco2lem7  33208  fracfld  33384  linds2eq  33456  dfufd2lem  33624  ply1dg3rt0irred  33659  ig1pmindeg  33677  esplymhp  33727  pconnconn  35429  irrdifflemf  37655  osumcllem11N  40426  dochexmidlem8  41927  sticksstones22  42621  exp11d  42772  remul01  42853  fnchoice  45478