Theorem pm2.21ddne 3039

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  sgnsub  15265  sgnmulsgn  15268  cshwshashlem2  17280  chnub  18802  chnccat  18806  dprdsn  20258  ablsimpgfind  20332  coseq00topi  26837  tglndim0  29103  ncolncol  29121  footne  29204  sgnmulsgp  33470  s3f1  33558  cycpmco2lem7  33740  fracfld  33917  linds2eq  33983  dfufd2lem  34128  ply1dg3rt0irred  34163  ig1pmindeg  34181  esplymhp  34247  pconnconn  36083  irrdifflemf  38340  osumcllem11N  41117  dochexmidlem8  42618  sticksstones22  43312  exp11d  43477  remul01  43552  fnchoice  46140