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  3040  smo11  8365  ackbij1lem16  10305  cfsmolem  10341  domtriomlem  10513  konigthlem  10646  grur1  10898  uzdisj  13724  nn0disj  13771  ccatf1  14729  sgnmul  15253  sgnmulsgn  15255  chnccats1  18792  chnccat  18793  psgnunilem2  19702  nmoleub2lem3  25429  i1f0  26001  itg2const2  26055  bposlem3  27606  bposlem9  27612  pntpbnd1  27906  infdesc  27960  prlngmolem2  29424  sgnmulsgp  33416  fzto1st1  33656  cycpmco2lem5  33684  mxidlirred  33990  rprmdvdspow  34058  1arithufd  34073  0mplrim  34139  esumpcvgval  34703  signstfvneq0  35194  derangsn  35914  heiborlem8  38732  lkrpssN  40200  cdleme27a  41404  aks4d1p3  43108  aks4d1p5  43110  aks4d1p8  43117  primrootlekpowne0  43135  primrootspoweq0  43136  sticksstones22  43198  aks6d1c6lem3  43202  aks6d1c6lem4  43203  aks6d1c7lem2  43211  unitscyglem2  43226  unitscyglem4  43228  aks5lem8  43231  pellfundex  43872  monotoddzzfi  43928  jm2.23  43982  rp-isfinite6  44503  r1rankcld  45214  iccpartiltu  48473  iccpartigtl  48474  pgn4cyclex  49193