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  3044  smo11  8353  ackbij1lem16  10229  cfsmolem  10265  domtriomlem  10437  konigthlem  10564  grur1  10816  uzdisj  13638  nn0disj  13685  ccatf1  14642  sgnmul  15164  sgnmulsgn  15166  chnccats1  18699  chnccat  18700  psgnunilem2  19589  nmoleub2lem3  25305  i1f0  25877  itg2const2  25931  bposlem3  27481  bposlem9  27487  pntpbnd1  27781  prlngmolem2  29234  sgnmulsgp  33222  fzto1st1  33462  cycpmco2lem5  33490  mxidlirred  33795  rprmdvdspow  33863  1arithufd  33878  0mplrim  33944  esumpcvgval  34508  signstfvneq0  35000  derangsn  35675  heiborlem8  38502  lkrpssN  39970  cdleme27a  41174  aks4d1p3  42878  aks4d1p5  42880  aks4d1p8  42887  primrootlekpowne0  42905  primrootspoweq0  42906  sticksstones22  42968  aks6d1c6lem3  42972  aks6d1c6lem4  42973  aks6d1c7lem2  42981  unitscyglem2  42996  unitscyglem4  42998  aks5lem8  43001  infdesc  43408  pellfundex  43646  monotoddzzfi  43702  jm2.23  43756  rp-isfinite6  44277  r1rankcld  44988  iccpartiltu  48204  iccpartigtl  48205  pgn4cyclex  48924