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  1562  pm2.21ddne  3010  smo11  8335  ackbij1lem16  10193  cfsmolem  10229  domtriomlem  10401  konigthlem  10527  grur1  10779  uzdisj  13564  nn0disj  13611  psgnunilem2  19431  nmoleub2lem3  25021  i1f0  25594  itg2const2  25648  bposlem3  27203  bposlem9  27209  pntpbnd1  27503  sgnmul  32766  sgnmulsgn  32773  sgnmulsgp  32774  ccatf1  32876  chnccats1  32947  fzto1st1  33065  cycpmco2lem5  33093  mxidlirred  33449  rprmdvdspow  33510  1arithufd  33525  esumpcvgval  34074  signstfvneq0  34569  derangsn  35157  heiborlem8  37807  lkrpssN  39151  cdleme27a  40356  aks4d1p3  42061  aks4d1p5  42063  aks4d1p8  42070  primrootlekpowne0  42088  primrootspoweq0  42089  sticksstones22  42151  aks6d1c6lem3  42155  aks6d1c6lem4  42156  aks6d1c7lem2  42164  unitscyglem2  42179  unitscyglem4  42181  aks5lem8  42184  infdesc  42624  pellfundex  42867  monotoddzzfi  42924  jm2.23  42978  rp-isfinite6  43500  r1rankcld  44213  iccpartiltu  47413  iccpartigtl  47414  pgn4cyclex  48106