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  1564  pm2.21ddne  3027  smo11  8364  ackbij1lem16  10230  cfsmolem  10265  domtriomlem  10437  konigthlem  10563  grur1  10815  uzdisj  13574  nn0disj  13617  psgnunilem2  19363  nmoleub2lem3  24631  i1f0  25204  itg2const2  25259  bposlem3  26789  bposlem9  26795  pntpbnd1  27089  ccatf1  32115  fzto1st1  32261  cycpmco2lem5  32289  mxidlirred  32588  esumpcvgval  33076  sgnmul  33541  sgnmulsgn  33548  sgnmulsgp  33549  signstfvneq0  33583  derangsn  34161  heiborlem8  36686  lkrpssN  38033  cdleme27a  39238  aks4d1p3  40943  aks4d1p5  40945  aks4d1p8  40952  sticksstones22  40984  infdesc  41385  pellfundex  41624  monotoddzzfi  41681  jm2.23  41735  rp-isfinite6  42269  r1rankcld  42990  iccpartiltu  46090  iccpartigtl  46091