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 1570   ≠ 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  15179  sgnmulsgn  15182  cshwshashlem2  17188  chnub  18710  chnccat  18714  dprdsn  20165  ablsimpgfind  20239  coseq00topi  26740  tglndim0  28976  ncolncol  28994  footne  29077  sgnmulsgp  33302  s3f1  33390  cycpmco2lem7  33572  fracfld  33749  linds2eq  33814  dfufd2lem  33959  ply1dg3rt0irred  33994  ig1pmindeg  34012  esplymhp  34078  pconnconn  35810  irrdifflemf  38077  osumcllem11N  40839  dochexmidlem8  42340  sticksstones22  43034  exp11d  43201  remul01  43282  fnchoice  45863