Theorem pm2.21dd 198

Description: A contradiction implies anything. Deduction from pm2.21 124. (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 196	. 2 ⊢ ¬ 𝜑
4	3	pm2.21i 120	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.21fal  1592  pm2.21ddne  3043  smo11  8410  ackbij1lem16  10351  cfsmolem  10387  domtriomlem  10559  konigthlem  10692  grur1  10944  uzdisj  13771  nn0disj  13818  ccatf1  14777  sgnmul  15303  sgnmulsgn  15305  chnccats1  18849  chnccat  18850  psgnunilem2  19760  nmoleub2lem3  25491  i1f0  26063  itg2const2  26117  bposlem3  27670  bposlem9  27676  pntpbnd1  27970  infdesc  28024  prlngmolem2  29488  tgextahp  33130  tgextan  33136  sgnmulsgp  33519  fzto1st1  33762  cycpmco2lem5  33790  mxidlirred  34101  rprmdvdspow  34169  1arithufd  34184  0mplrim  34257  esumpcvgval  34821  signstfvneq0  35312  derangsn  36143  heiborlem8  39018  lkrpssN  40486  cdleme27a  41690  aks4d1p3  43394  aks4d1p5  43396  aks4d1p8  43403  primrootlekpowne0  43421  primrootspoweq0  43422  sticksstones22  43484  aks6d1c6lem3  43488  aks6d1c6lem4  43489  aks6d1c7lem2  43497  unitscyglem2  43512  unitscyglem4  43514  aks5lem8  43517  pellfundex  44159  monotoddzzfi  44215  jm2.23  44269  rp-isfinite6  44780  r1rankcld  45490  iccpartiltu  48777  iccpartigtl  48778  pgn4cyclex  49497