Theorem pm2.21dd 194

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 193	. 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  1561  pm2.21ddne  3029  smo11  8195  ackbij1lem16  9991  cfsmolem  10026  domtriomlem  10198  konigthlem  10324  grur1  10576  uzdisj  13329  nn0disj  13372  psgnunilem2  19103  nmoleub2lem3  24278  i1f0  24851  itg2const2  24906  bposlem3  26434  bposlem9  26440  pntpbnd1  26734  ccatf1  31223  fzto1st1  31369  cycpmco2lem5  31397  esumpcvgval  32046  sgnmul  32509  sgnmulsgn  32516  sgnmulsgp  32517  signstfvneq0  32551  derangsn  33132  heiborlem8  35976  lkrpssN  37177  cdleme27a  38381  aks4d1p3  40086  aks4d1p5  40088  aks4d1p8  40095  sticksstones22  40124  infdesc  40480  pellfundex  40708  monotoddzzfi  40764  jm2.23  40818  rp-isfinite6  41125  r1rankcld  41849  iccpartiltu  44874  iccpartigtl  44875