Theorem pm2.21dd 187

Description: A contradiction implies anything. Deduction from pm2.21 121. (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 186	. 2 ⊢ ¬ 𝜑
4	3	pm2.21i 117	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  1679  pm2.21ddne  3083  smo11  7727  ackbij1lem16  9372  cfsmolem  9407  domtriomlem  9579  konigthlem  9705  grur1  9957  uzdisj  12707  nn0disj  12750  psgnunilem2  18266  nmoleub2lem3  23284  i1f0  23853  itg2const2  23907  bposlem3  25424  bposlem9  25430  pntpbnd1  25688  fzto1st1  30386  esumpcvgval  30674  sgnmul  31139  sgnmulsgn  31146  sgnmulsgp  31147  signstfvneq0  31186  derangsn  31687  heiborlem8  34152  lkrpssN  35231  cdleme27a  36435  pellfundex  38287  monotoddzzfi  38343  jm2.23  38399  rp-isfinite6  38698  iccpartiltu  42239  iccpartigtl  42240