Theorem pm2.21ddne 3015

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2931

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 2932

This theorem is referenced by:  cshwshashlem2  17117  dprdsn  20025  ablsimpgfind  20099  coseq00topi  26481  tglndim0  28574  ncolncol  28591  footne  28668  s3f1  32876  chnub  32946  cycpmco2lem7  33096  fracfld  33255  linds2eq  33349  dfufd2lem  33517  ply1dg3rt0irred  33547  ig1pmindeg  33562  sgnsub  34522  sgnmulsgn  34527  sgnmulsgp  34528  pconnconn  35211  irrdifflemf  37301  osumcllem11N  39943  dochexmidlem8  41444  sticksstones22  42144  exp11d  42340  remul01  42416  fnchoice  45006