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  1591  pm2.21ddne  3041  smo11  8349  ackbij1lem16  10224  cfsmolem  10260  domtriomlem  10432  konigthlem  10559  grur1  10811  uzdisj  13632  nn0disj  13679  sgnmul  15151  sgnmulsgn  15153  chnccats1  18687  chnccat  18688  psgnunilem2  19571  nmoleub2lem3  25285  i1f0  25857  itg2const2  25911  bposlem3  27461  bposlem9  27467  pntpbnd1  27761  prlngmolem2  29214  sgnmulsgp  33187  ccatf1  33278  fzto1st1  33431  cycpmco2lem5  33459  mxidlirred  33764  rprmdvdspow  33832  1arithufd  33847  0mplrim  33913  esumpcvgval  34477  signstfvneq0  34968  derangsn  35670  heiborlem8  38497  lkrpssN  39965  cdleme27a  41169  aks4d1p3  42873  aks4d1p5  42875  aks4d1p8  42882  primrootlekpowne0  42900  primrootspoweq0  42901  sticksstones22  42963  aks6d1c6lem3  42967  aks6d1c6lem4  42968  aks6d1c7lem2  42976  unitscyglem2  42991  unitscyglem4  42993  aks5lem8  42996  infdesc  43403  pellfundex  43641  monotoddzzfi  43697  jm2.23  43751  rp-isfinite6  44272  r1rankcld  44983  iccpartiltu  48199  iccpartigtl  48200  pgn4cyclex  48919