Theorem pm2.21dd 197

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 195	. 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  1581  pm2.21ddne  3040  smo11  8329  ackbij1lem16  10184  cfsmolem  10221  domtriomlem  10393  konigthlem  10520  grur1  10772  uzdisj  13596  nn0disj  13643  sgnmul  15111  sgnmulsgn  15113  chnccats1  18648  chnccat  18649  psgnunilem2  19526  nmoleub2lem3  25165  i1f0  25737  itg2const2  25791  bposlem3  27338  bposlem9  27344  pntpbnd1  27638  sgnmulsgp  32995  ccatf1  33088  fzto1st1  33243  cycpmco2lem5  33271  mxidlirred  33621  rprmdvdspow  33690  1arithufd  33705  0mplrim  33772  esumpcvgval  34336  signstfvneq0  34827  derangsn  35481  heiborlem8  38278  lkrpssN  39748  cdleme27a  40952  aks4d1p3  42656  aks4d1p5  42658  aks4d1p8  42665  primrootlekpowne0  42683  primrootspoweq0  42684  sticksstones22  42746  aks6d1c6lem3  42750  aks6d1c6lem4  42751  aks6d1c7lem2  42759  unitscyglem2  42774  unitscyglem4  42776  aks5lem8  42779  infdesc  43186  pellfundex  43424  monotoddzzfi  43480  jm2.23  43534  rp-isfinite6  44055  r1rankcld  44768  iccpartiltu  47989  iccpartigtl  47990  pgn4cyclex  48709