Theorem pm2.21dd 194

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 193	. 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  1555  pm2.21ddne  3023  smo11  8391  ackbij1lem16  10266  cfsmolem  10301  domtriomlem  10473  konigthlem  10599  grur1  10851  uzdisj  13614  nn0disj  13657  psgnunilem2  19457  nmoleub2lem3  25062  i1f0  25636  itg2const2  25691  bposlem3  27239  bposlem9  27245  pntpbnd1  27539  ccatf1  32693  fzto1st1  32844  cycpmco2lem5  32872  mxidlirred  33210  rprmdvdspow  33272  esumpcvgval  33730  sgnmul  34195  sgnmulsgn  34202  sgnmulsgp  34203  signstfvneq0  34237  derangsn  34813  heiborlem8  37324  lkrpssN  38667  cdleme27a  39872  aks4d1p3  41581  aks4d1p5  41583  aks4d1p8  41590  primrootlekpowne0  41608  primrootspoweq0  41609  sticksstones22  41672  aks6d1c6lem3  41676  aks6d1c6lem4  41677  aks6d1c7lem2  41685  infdesc  42098  pellfundex  42337  monotoddzzfi  42394  jm2.23  42448  rp-isfinite6  42979  r1rankcld  43699  iccpartiltu  46791  iccpartigtl  46792