Theorem pm2.21ddne 3044

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2960

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 2961

This theorem is used by:  sgnsub  15162  sgnmulsgn  15165  cshwshashlem2  17173  chnub  18695  chnccat  18699  dprdsn  20131  ablsimpgfind  20205  coseq00topi  26696  tglndim0  28931  ncolncol  28949  footne  29032  sgnmulsgp  33205  s3f1  33293  cycpmco2lem7  33475  fracfld  33652  linds2eq  33717  dfufd2lem  33862  ply1dg3rt0irred  33897  ig1pmindeg  33915  esplymhp  33981  pconnconn  35736  irrdifflemf  38002  osumcllem11N  40773  dochexmidlem8  42274  sticksstones22  42968  exp11d  43120  remul01  43201  fnchoice  45782