Theorem pm2.21ddne 3042

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

Syntax hints:   → wi 4   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  sgnsub  15145  sgnmulsgn  15148  cshwshashlem2  17157  chnub  18679  chnccat  18683  dprdsn  20109  ablsimpgfind  20183  coseq00topi  26648  tglndim0  28883  ncolncol  28901  footne  28984  sgnmulsgp  33157  s3f1  33248  cycpmco2lem7  33433  fracfld  33610  linds2eq  33675  dfufd2lem  33820  ply1dg3rt0irred  33855  ig1pmindeg  33873  esplymhp  33939  pconnconn  35704  irrdifflemf  37950  osumcllem11N  40721  dochexmidlem8  42222  sticksstones22  42916  exp11d  43068  remul01  43149  fnchoice  45732