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 196	. 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  1555  pm2.21ddne  3101  smo11  7995  ackbij1lem16  9651  cfsmolem  9686  domtriomlem  9858  konigthlem  9984  grur1  10236  uzdisj  12974  nn0disj  13017  psgnunilem2  18617  nmoleub2lem3  23713  i1f0  24282  itg2const2  24336  bposlem3  25856  bposlem9  25862  pntpbnd1  26156  ccatf1  30620  fzto1st1  30739  cycpmco2lem5  30767  esumpcvgval  31332  sgnmul  31795  sgnmulsgn  31802  sgnmulsgp  31803  signstfvneq0  31837  derangsn  32412  heiborlem8  35090  lkrpssN  36293  cdleme27a  37497  pellfundex  39476  monotoddzzfi  39532  jm2.23  39586  rp-isfinite6  39877  r1rankcld  40560  iccpartiltu  43575  iccpartigtl  43576