Theorem pm2.21ddne 3010

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2926

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 2927

This theorem is referenced by:  cshwshashlem2  17074  dprdsn  19975  ablsimpgfind  20049  coseq00topi  26418  tglndim0  28563  ncolncol  28580  footne  28657  sgnsub  32769  sgnmulsgn  32774  sgnmulsgp  32775  s3f1  32875  chnub  32945  cycpmco2lem7  33096  fracfld  33265  linds2eq  33359  dfufd2lem  33527  ply1dg3rt0irred  33558  ig1pmindeg  33574  pconnconn  35225  irrdifflemf  37320  osumcllem11N  39967  dochexmidlem8  41468  sticksstones22  42163  exp11d  42321  remul01  42402  fnchoice  45030