Theorem pm2.21ddne 3012

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928

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 207  df-ne 2929

This theorem is referenced by:  cshwshashlem2  17005  chnub  18525  chnccat  18529  dprdsn  19948  ablsimpgfind  20022  coseq00topi  26436  tglndim0  28605  ncolncol  28622  footne  28699  sgnsub  32815  sgnmulsgn  32820  sgnmulsgp  32821  s3f1  32923  cycpmco2lem7  33096  fracfld  33269  linds2eq  33341  dfufd2lem  33509  ply1dg3rt0irred  33541  ig1pmindeg  33557  esplymhp  33584  pconnconn  35263  irrdifflemf  37358  osumcllem11N  40004  dochexmidlem8  41505  sticksstones22  42200  exp11d  42358  remul01  42439  fnchoice  45065