Theorem pm2.21dd 198

Description: A contradiction implies anything. Deduction from pm2.21 124. (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 120	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  1589  pm2.21ddne  3048  smo11  8347  ackbij1lem16  10213  cfsmolem  10250  domtriomlem  10422  konigthlem  10549  grur1  10801  uzdisj  13621  nn0disj  13668  sgnmul  15140  sgnmulsgn  15142  chnccats1  18677  chnccat  18678  psgnunilem2  19561  nmoleub2lem3  25239  i1f0  25811  itg2const2  25865  bposlem3  27412  bposlem9  27418  pntpbnd1  27712  prlngmolem2  29152  sgnmulsgp  33113  ccatf1  33206  fzto1st1  33359  cycpmco2lem5  33387  mxidlirred  33696  rprmdvdspow  33764  1arithufd  33779  0mplrim  33845  esumpcvgval  34409  signstfvneq0  34900  derangsn  35557  heiborlem8  38352  lkrpssN  39822  cdleme27a  41026  aks4d1p3  42730  aks4d1p5  42732  aks4d1p8  42739  primrootlekpowne0  42757  primrootspoweq0  42758  sticksstones22  42820  aks6d1c6lem3  42824  aks6d1c6lem4  42825  aks6d1c7lem2  42833  unitscyglem2  42848  unitscyglem4  42850  aks5lem8  42853  infdesc  43262  pellfundex  43500  monotoddzzfi  43556  jm2.23  43610  rp-isfinite6  44131  r1rankcld  44842  iccpartiltu  48055  iccpartigtl  48056  pgn4cyclex  48775