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  1559  pm2.21ddne  3103  smo11  8003  ackbij1lem16  9659  cfsmolem  9694  domtriomlem  9866  konigthlem  9992  grur1  10244  uzdisj  12983  nn0disj  13026  psgnunilem2  18625  nmoleub2lem3  23721  i1f0  24290  itg2const2  24344  bposlem3  25864  bposlem9  25870  pntpbnd1  26164  ccatf1  30627  fzto1st1  30746  cycpmco2lem5  30774  esumpcvgval  31339  sgnmul  31802  sgnmulsgn  31809  sgnmulsgp  31810  signstfvneq0  31844  derangsn  32419  heiborlem8  35098  lkrpssN  36301  cdleme27a  37505  pellfundex  39490  monotoddzzfi  39546  jm2.23  39600  rp-isfinite6  39891  r1rankcld  40574  iccpartiltu  43589  iccpartigtl  43590