Theorem pm2.21ddne 3043

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

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

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 2960

This theorem is used by:  sgnsub  15302  sgnmulsgn  15305  cshwshashlem2  17318  chnub  18846  chnccat  18850  dprdsn  20303  ablsimpgfind  20377  coseq00topi  26888  tglndim0  29154  ncolncol  29172  footne  29255  sgnmulsgp  33519  s3f1  33607  cycpmco2lem7  33792  fracfld  33974  linds2eq  34040  dfufd2lem  34185  ply1dg3rt0irred  34219  ig1pmindeg  34237  esplymhp  34311  pconnconn  36204  irrdifflemf  38514  osumcllem11N  41289  dochexmidlem8  42790  sticksstones22  43484  exp11d  43649  remul01  43724  fnchoice  46320