Theorem pm2.21ddne 3032

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  cshwshashlem2  17144  dprdsn  20080  ablsimpgfind  20154  coseq00topi  26562  tglndim0  28655  ncolncol  28672  footne  28749  s3f1  32913  chnub  32984  cycpmco2lem7  33125  fracfld  33275  linds2eq  33374  dfufd2lem  33542  ply1dg3rt0irred  33572  ig1pmindeg  33587  sgnsub  34509  sgnmulsgn  34514  sgnmulsgp  34515  pconnconn  35199  irrdifflemf  37291  osumcllem11N  39923  dochexmidlem8  41424  sticksstones22  42125  exp11d  42313  remul01  42383  fnchoice  44929