Theorem pm2.21dd 198

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 197	. 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  1560  pm2.21ddne  3071  smo11  7984  ackbij1lem16  9646  cfsmolem  9681  domtriomlem  9853  konigthlem  9979  grur1  10231  uzdisj  12975  nn0disj  13018  psgnunilem2  18615  nmoleub2lem3  23720  i1f0  24291  itg2const2  24345  bposlem3  25870  bposlem9  25876  pntpbnd1  26170  ccatf1  30651  fzto1st1  30794  cycpmco2lem5  30822  esumpcvgval  31447  sgnmul  31910  sgnmulsgn  31917  sgnmulsgp  31918  signstfvneq0  31952  derangsn  32530  heiborlem8  35256  lkrpssN  36459  cdleme27a  37663  pellfundex  39827  monotoddzzfi  39883  jm2.23  39937  rp-isfinite6  40226  r1rankcld  40939  iccpartiltu  43939  iccpartigtl  43940