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  17036  chnub  18557  chnccat  18561  dprdsn  19979  ablsimpgfind  20053  coseq00topi  26479  tglndim0  28713  ncolncol  28730  footne  28807  sgnsub  32928  sgnmulsgn  32933  sgnmulsgp  32934  s3f1  33039  cycpmco2lem7  33225  fracfld  33401  linds2eq  33473  dfufd2lem  33641  ply1dg3rt0irred  33676  ig1pmindeg  33694  esplymhp  33744  pconnconn  35444  irrdifflemf  37577  osumcllem11N  40339  dochexmidlem8  41840  sticksstones22  42535  exp11d  42693  remul01  42774  fnchoice  45386