Theorem pm2.21dd 195

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 194	. 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  1563  pm2.21ddne  3012  smo11  8279  ackbij1lem16  10120  cfsmolem  10156  domtriomlem  10328  konigthlem  10454  grur1  10706  uzdisj  13492  nn0disj  13539  chnccats1  18526  chnccat  18527  psgnunilem2  19402  nmoleub2lem3  25037  i1f0  25610  itg2const2  25664  bposlem3  27219  bposlem9  27225  pntpbnd1  27519  sgnmul  32810  sgnmulsgn  32817  sgnmulsgp  32818  ccatf1  32922  fzto1st1  33063  cycpmco2lem5  33091  mxidlirred  33429  rprmdvdspow  33490  1arithufd  33505  esumpcvgval  34083  signstfvneq0  34577  derangsn  35206  heiborlem8  37858  lkrpssN  39202  cdleme27a  40406  aks4d1p3  42111  aks4d1p5  42113  aks4d1p8  42120  primrootlekpowne0  42138  primrootspoweq0  42139  sticksstones22  42201  aks6d1c6lem3  42205  aks6d1c6lem4  42206  aks6d1c7lem2  42214  unitscyglem2  42229  unitscyglem4  42231  aks5lem8  42234  infdesc  42676  pellfundex  42919  monotoddzzfi  42975  jm2.23  43029  rp-isfinite6  43551  r1rankcld  44264  iccpartiltu  47453  iccpartigtl  47454  pgn4cyclex  48157