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  1562  pm2.21ddne  3025  smo11  8367  ackbij1lem16  10233  cfsmolem  10268  domtriomlem  10440  konigthlem  10566  grur1  10818  uzdisj  13579  nn0disj  13622  psgnunilem2  19405  nmoleub2lem3  24863  i1f0  25437  itg2const2  25492  bposlem3  27026  bposlem9  27032  pntpbnd1  27326  ccatf1  32383  fzto1st1  32532  cycpmco2lem5  32560  mxidlirred  32863  esumpcvgval  33375  sgnmul  33840  sgnmulsgn  33847  sgnmulsgp  33848  signstfvneq0  33882  derangsn  34460  heiborlem8  36990  lkrpssN  38337  cdleme27a  39542  aks4d1p3  41250  aks4d1p5  41252  aks4d1p8  41259  sticksstones22  41291  infdesc  41688  pellfundex  41927  monotoddzzfi  41984  jm2.23  42038  rp-isfinite6  42572  r1rankcld  43293  iccpartiltu  46389  iccpartigtl  46390