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  1564  pm2.21ddne  3017  smo11  8306  ackbij1lem16  10156  cfsmolem  10192  domtriomlem  10364  konigthlem  10491  grur1  10743  uzdisj  13525  nn0disj  13572  chnccats1  18560  chnccat  18561  psgnunilem2  19436  nmoleub2lem3  25083  i1f0  25656  itg2const2  25710  bposlem3  27265  bposlem9  27271  pntpbnd1  27565  sgnmul  32927  sgnmulsgn  32934  sgnmulsgp  32935  ccatf1  33042  fzto1st1  33196  cycpmco2lem5  33224  mxidlirred  33565  rprmdvdspow  33626  1arithufd  33641  esumpcvgval  34256  signstfvneq0  34750  derangsn  35386  heiborlem8  38069  lkrpssN  39539  cdleme27a  40743  aks4d1p3  42448  aks4d1p5  42450  aks4d1p8  42457  primrootlekpowne0  42475  primrootspoweq0  42476  sticksstones22  42538  aks6d1c6lem3  42542  aks6d1c6lem4  42543  aks6d1c7lem2  42551  unitscyglem2  42566  unitscyglem4  42568  aks5lem8  42571  infdesc  43001  pellfundex  43243  monotoddzzfi  43299  jm2.23  43353  rp-isfinite6  43874  r1rankcld  44587  iccpartiltu  47782  iccpartigtl  47783  pgn4cyclex  48486