Theorem pm2.21dd 198

Description: A contradiction implies anything. Deduction from pm2.21 124. (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 196	. 2 ⊢ ¬ 𝜑
4	3	pm2.21i 120	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.21fal  1592  pm2.21ddne  3039  smo11  8353  ackbij1lem16  10236  cfsmolem  10272  domtriomlem  10444  konigthlem  10577  grur1  10829  uzdisj  13652  nn0disj  13699  ccatf1  14656  sgnmul  15180  sgnmulsgn  15182  chnccats1  18713  chnccat  18714  psgnunilem2  19622  nmoleub2lem3  25343  i1f0  25915  itg2const2  25969  bposlem3  27522  bposlem9  27528  pntpbnd1  27822  prlngmolem2  29310  sgnmulsgp  33302  fzto1st1  33542  cycpmco2lem5  33570  mxidlirred  33875  rprmdvdspow  33943  1arithufd  33958  0mplrim  34024  esumpcvgval  34588  signstfvneq0  35080  derangsn  35749  heiborlem8  38568  lkrpssN  40036  cdleme27a  41240  aks4d1p3  42944  aks4d1p5  42946  aks4d1p8  42953  primrootlekpowne0  42971  primrootspoweq0  42972  sticksstones22  43034  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c7lem2  43047  unitscyglem2  43062  unitscyglem4  43064  aks5lem8  43067  infdesc  43489  pellfundex  43727  monotoddzzfi  43783  jm2.23  43837  rp-isfinite6  44358  r1rankcld  45069  iccpartiltu  48322  iccpartigtl  48323  pgn4cyclex  49042