Theorem pm2.21dd 194

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 193	. 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  1561  pm2.21ddne  3028  smo11  8166  ackbij1lem16  9922  cfsmolem  9957  domtriomlem  10129  konigthlem  10255  grur1  10507  uzdisj  13258  nn0disj  13301  psgnunilem2  19018  nmoleub2lem3  24184  i1f0  24756  itg2const2  24811  bposlem3  26339  bposlem9  26345  pntpbnd1  26639  ccatf1  31125  fzto1st1  31271  cycpmco2lem5  31299  esumpcvgval  31946  sgnmul  32409  sgnmulsgn  32416  sgnmulsgp  32417  signstfvneq0  32451  derangsn  33032  heiborlem8  35903  lkrpssN  37104  cdleme27a  38308  aks4d1p3  40014  aks4d1p5  40016  aks4d1p8  40023  sticksstones22  40052  infdesc  40396  pellfundex  40624  monotoddzzfi  40680  jm2.23  40734  rp-isfinite6  41023  r1rankcld  41738  iccpartiltu  44762  iccpartigtl  44763