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  1563  pm2.21ddne  3010  smo11  8279  ackbij1lem16  10117  cfsmolem  10153  domtriomlem  10325  konigthlem  10451  grur1  10703  uzdisj  13489  nn0disj  13536  chnccats1  18523  chnccat  18524  psgnunilem2  19400  nmoleub2lem3  25035  i1f0  25608  itg2const2  25662  bposlem3  27217  bposlem9  27223  pntpbnd1  27517  sgnmul  32808  sgnmulsgn  32815  sgnmulsgp  32816  ccatf1  32920  fzto1st1  33061  cycpmco2lem5  33089  mxidlirred  33427  rprmdvdspow  33488  1arithufd  33503  esumpcvgval  34081  signstfvneq0  34575  derangsn  35182  heiborlem8  37837  lkrpssN  39181  cdleme27a  40385  aks4d1p3  42090  aks4d1p5  42092  aks4d1p8  42099  primrootlekpowne0  42117  primrootspoweq0  42118  sticksstones22  42180  aks6d1c6lem3  42184  aks6d1c6lem4  42185  aks6d1c7lem2  42193  unitscyglem2  42208  unitscyglem4  42210  aks5lem8  42213  infdesc  42655  pellfundex  42898  monotoddzzfi  42954  jm2.23  43008  rp-isfinite6  43530  r1rankcld  44243  iccpartiltu  47432  iccpartigtl  47433  pgn4cyclex  48136