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  1563  pm2.21ddne  3026  smo11  8366  ackbij1lem16  10232  cfsmolem  10267  domtriomlem  10439  konigthlem  10565  grur1  10817  uzdisj  13576  nn0disj  13619  psgnunilem2  19365  nmoleub2lem3  24638  i1f0  25211  itg2const2  25266  bposlem3  26796  bposlem9  26802  pntpbnd1  27096  ccatf1  32153  fzto1st1  32302  cycpmco2lem5  32330  mxidlirred  32633  esumpcvgval  33145  sgnmul  33610  sgnmulsgn  33617  sgnmulsgp  33618  signstfvneq0  33652  derangsn  34230  heiborlem8  36772  lkrpssN  38119  cdleme27a  39324  aks4d1p3  41029  aks4d1p5  41031  aks4d1p8  41038  sticksstones22  41070  infdesc  41467  pellfundex  41706  monotoddzzfi  41763  jm2.23  41817  rp-isfinite6  42351  r1rankcld  43072  iccpartiltu  46169  iccpartigtl  46170