Theorem pm2.21dd 195

Description: A contradiction implies anything. Deduction from pm2.21 123. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.)

Hypotheses

Ref	Expression
pm2.21dd.1	⊢ (𝜑 → 𝜓)
pm2.21dd.2	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.21dd	⊢ (𝜑 → 𝜒)

Proof of Theorem pm2.21dd

Step	Hyp	Ref	Expression
1		pm2.21dd.1	. . 3 ⊢ (𝜑 → 𝜓)
2		pm2.21dd.2	. . 3 ⊢ (𝜑 → ¬ 𝜓)
3	1, 2	pm2.65i 194	. 2 ⊢ ¬ 𝜑
4	3	pm2.21i 119	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.21fal  1559  pm2.21ddne  3028  smo11  8416  ackbij1lem16  10299  cfsmolem  10335  domtriomlem  10507  konigthlem  10633  grur1  10885  uzdisj  13653  nn0disj  13697  psgnunilem2  19532  nmoleub2lem3  25160  i1f0  25734  itg2const2  25789  bposlem3  27339  bposlem9  27345  pntpbnd1  27639  ccatf1  32907  fzto1st1  33087  cycpmco2lem5  33115  mxidlirred  33457  rprmdvdspow  33518  1arithufd  33533  esumpcvgval  34034  sgnmul  34499  sgnmulsgn  34506  sgnmulsgp  34507  signstfvneq0  34541  derangsn  35130  heiborlem8  37727  lkrpssN  39068  cdleme27a  40273  aks4d1p3  41984  aks4d1p5  41986  aks4d1p8  41993  primrootlekpowne0  42011  primrootspoweq0  42012  sticksstones22  42074  aks6d1c6lem3  42078  aks6d1c6lem4  42079  aks6d1c7lem2  42087  unitscyglem2  42102  unitscyglem4  42104  aks5lem8  42107  infdesc  42532  pellfundex  42780  monotoddzzfi  42837  jm2.23  42891  rp-isfinite6  43421  r1rankcld  44141  iccpartiltu  47229  iccpartigtl  47230