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  7732  ackbij1lem16  9379  cfsmolem  9414  domtriomlem  9586  konigthlem  9712  grur1  9964  uzdisj  12714  nn0disj  12757  psgnunilem2  18273  nmoleub2lem3  23291  i1f0  23860  itg2const2  23914  bposlem3  25431  bposlem9  25437  pntpbnd1  25695  fzto1st1  30393  esumpcvgval  30681  sgnmul  31146  sgnmulsgn  31153  sgnmulsgp  31154  signstfvneq0  31193  derangsn  31694  heiborlem8  34154  lkrpssN  35233  cdleme27a  36437  pellfundex  38289  monotoddzzfi  38345  jm2.23  38401  rp-isfinite6  38700  iccpartiltu  42240  iccpartigtl  42241