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  3032  smo11  8422  ackbij1lem16  10305  cfsmolem  10341  domtriomlem  10513  konigthlem  10639  grur1  10891  uzdisj  13659  nn0disj  13703  psgnunilem2  19539  nmoleub2lem3  25169  i1f0  25743  itg2const2  25798  bposlem3  27350  bposlem9  27356  pntpbnd1  27650  ccatf1  32917  fzto1st1  33097  cycpmco2lem5  33125  mxidlirred  33467  rprmdvdspow  33528  1arithufd  33543  esumpcvgval  34044  sgnmul  34509  sgnmulsgn  34516  sgnmulsgp  34517  signstfvneq0  34551  derangsn  35140  heiborlem8  37780  lkrpssN  39121  cdleme27a  40326  aks4d1p3  42037  aks4d1p5  42039  aks4d1p8  42046  primrootlekpowne0  42064  primrootspoweq0  42065  sticksstones22  42127  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c7lem2  42140  unitscyglem2  42155  unitscyglem4  42157  aks5lem8  42160  infdesc  42600  pellfundex  42844  monotoddzzfi  42901  jm2.23  42955  rp-isfinite6  43482  r1rankcld  44202  iccpartiltu  47298  iccpartigtl  47299