Theorem pm2.21dd 196

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 195	. 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  1569  pm2.21ddne  3018  smo11  8294  ackbij1lem16  10147  cfsmolem  10183  domtriomlem  10355  konigthlem  10482  grur1  10734  uzdisj  13542  nn0disj  13589  chnccats1  18582  chnccat  18583  psgnunilem2  19461  nmoleub2lem3  25100  i1f0  25672  itg2const2  25726  bposlem3  27267  bposlem9  27273  pntpbnd1  27567  sgnmul  32927  sgnmulsgn  32934  sgnmulsgp  32935  ccatf1  33028  fzto1st1  33183  cycpmco2lem5  33211  mxidlirred  33555  rprmdvdspow  33616  1arithufd  33631  0mplrim  33698  esumpcvgval  34262  signstfvneq0  34756  derangsn  35398  heiborlem8  38185  lkrpssN  39655  cdleme27a  40859  aks4d1p3  42563  aks4d1p5  42565  aks4d1p8  42572  primrootlekpowne0  42590  primrootspoweq0  42591  sticksstones22  42653  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c7lem2  42666  unitscyglem2  42681  unitscyglem4  42683  aks5lem8  42686  infdesc  43093  pellfundex  43331  monotoddzzfi  43387  jm2.23  43441  rp-isfinite6  43962  r1rankcld  44675  iccpartiltu  47897  iccpartigtl  47898  pgn4cyclex  48617