Theorem pm2.21ddne 3048

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

Syntax hints:   → wi 4   = wceq 1567   ≠ wne 2964

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 210  df-ne 2965

This theorem is referenced by:  sgnsub  15139  sgnmulsgn  15142  cshwshashlem2  17152  chnub  18674  chnccat  18678  dprdsn  20104  ablsimpgfind  20178  coseq00topi  26629  tglndim0  28860  ncolncol  28878  footne  28958  sgnmulsgp  33113  s3f1  33204  cycpmco2lem7  33389  fracfld  33568  linds2eq  33634  dfufd2lem  33780  ply1dg3rt0irred  33815  ig1pmindeg  33833  esplymhp  33899  pconnconn  35618  irrdifflemf  37852  osumcllem11N  40625  dochexmidlem8  42126  sticksstones22  42820  exp11d  42970  remul01  43051  fnchoice  45634