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  1561  pm2.21ddne  3015  smo11  8386  ackbij1lem16  10256  cfsmolem  10292  domtriomlem  10464  konigthlem  10590  grur1  10842  uzdisj  13619  nn0disj  13666  psgnunilem2  19481  nmoleub2lem3  25084  i1f0  25658  itg2const2  25712  bposlem3  27266  bposlem9  27272  pntpbnd1  27566  ccatf1  32873  chnccats1  32944  fzto1st1  33061  cycpmco2lem5  33089  mxidlirred  33435  rprmdvdspow  33496  1arithufd  33511  esumpcvgval  34038  sgnmul  34504  sgnmulsgn  34511  sgnmulsgp  34512  signstfvneq0  34546  derangsn  35134  heiborlem8  37784  lkrpssN  39123  cdleme27a  40328  aks4d1p3  42038  aks4d1p5  42040  aks4d1p8  42047  primrootlekpowne0  42065  primrootspoweq0  42066  sticksstones22  42128  aks6d1c6lem3  42132  aks6d1c6lem4  42133  aks6d1c7lem2  42141  unitscyglem2  42156  unitscyglem4  42158  aks5lem8  42161  infdesc  42616  pellfundex  42860  monotoddzzfi  42917  jm2.23  42971  rp-isfinite6  43493  r1rankcld  44207  iccpartiltu  47367  iccpartigtl  47368