Theorem pm2.21dd 195

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 194	. 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  3016  smo11  8296  ackbij1lem16  10144  cfsmolem  10180  domtriomlem  10352  konigthlem  10479  grur1  10731  uzdisj  13513  nn0disj  13560  chnccats1  18548  chnccat  18549  psgnunilem2  19424  nmoleub2lem3  25071  i1f0  25644  itg2const2  25698  bposlem3  27253  bposlem9  27259  pntpbnd1  27553  sgnmul  32916  sgnmulsgn  32923  sgnmulsgp  32924  ccatf1  33031  fzto1st1  33184  cycpmco2lem5  33212  mxidlirred  33553  rprmdvdspow  33614  1arithufd  33629  esumpcvgval  34235  signstfvneq0  34729  derangsn  35364  heiborlem8  38019  lkrpssN  39423  cdleme27a  40627  aks4d1p3  42332  aks4d1p5  42334  aks4d1p8  42341  primrootlekpowne0  42359  primrootspoweq0  42360  sticksstones22  42422  aks6d1c6lem3  42426  aks6d1c6lem4  42427  aks6d1c7lem2  42435  unitscyglem2  42450  unitscyglem4  42452  aks5lem8  42455  infdesc  42886  pellfundex  43128  monotoddzzfi  43184  jm2.23  43238  rp-isfinite6  43759  r1rankcld  44472  iccpartiltu  47668  iccpartigtl  47669  pgn4cyclex  48372