Theorem pm2.21ddne 3040

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

Syntax hints:   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  sgnsub  15110  sgnmulsgn  15113  cshwshashlem2  17123  chnub  18645  chnccat  18649  dprdsn  20069  ablsimpgfind  20143  coseq00topi  26555  tglndim0  28786  ncolncol  28803  footne  28880  sgnmulsgp  32995  s3f1  33086  cycpmco2lem7  33273  fracfld  33456  linds2eq  33528  dfufd2lem  33706  ply1dg3rt0irred  33741  ig1pmindeg  33759  esplymhp  33826  pconnconn  35542  irrdifflemf  37778  osumcllem11N  40551  dochexmidlem8  42052  sticksstones22  42746  exp11d  42896  remul01  42977  fnchoice  45570