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  1562  pm2.21ddne  3009  smo11  8310  ackbij1lem16  10163  cfsmolem  10199  domtriomlem  10371  konigthlem  10497  grur1  10749  uzdisj  13534  nn0disj  13581  psgnunilem2  19401  nmoleub2lem3  24991  i1f0  25564  itg2const2  25618  bposlem3  27173  bposlem9  27179  pntpbnd1  27473  sgnmul  32733  sgnmulsgn  32740  sgnmulsgp  32741  ccatf1  32843  chnccats1  32914  fzto1st1  33032  cycpmco2lem5  33060  mxidlirred  33416  rprmdvdspow  33477  1arithufd  33492  esumpcvgval  34041  signstfvneq0  34536  derangsn  35130  heiborlem8  37785  lkrpssN  39129  cdleme27a  40334  aks4d1p3  42039  aks4d1p5  42041  aks4d1p8  42048  primrootlekpowne0  42066  primrootspoweq0  42067  sticksstones22  42129  aks6d1c6lem3  42133  aks6d1c6lem4  42134  aks6d1c7lem2  42142  unitscyglem2  42157  unitscyglem4  42159  aks5lem8  42162  infdesc  42604  pellfundex  42847  monotoddzzfi  42904  jm2.23  42958  rp-isfinite6  43480  r1rankcld  44193  iccpartiltu  47396  iccpartigtl  47397  pgn4cyclex  48089