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  1561  pm2.21ddne  3026  smo11  8412  ackbij1lem16  10281  cfsmolem  10317  domtriomlem  10489  konigthlem  10615  grur1  10867  uzdisj  13643  nn0disj  13690  psgnunilem2  19537  nmoleub2lem3  25173  i1f0  25747  itg2const2  25802  bposlem3  27356  bposlem9  27362  pntpbnd1  27656  ccatf1  32950  fzto1st1  33137  cycpmco2lem5  33165  mxidlirred  33512  rprmdvdspow  33573  1arithufd  33588  esumpcvgval  34073  sgnmul  34538  sgnmulsgn  34545  sgnmulsgp  34546  signstfvneq0  34580  derangsn  35168  heiborlem8  37819  lkrpssN  39159  cdleme27a  40364  aks4d1p3  42074  aks4d1p5  42076  aks4d1p8  42083  primrootlekpowne0  42101  primrootspoweq0  42102  sticksstones22  42164  aks6d1c6lem3  42168  aks6d1c6lem4  42169  aks6d1c7lem2  42177  unitscyglem2  42192  unitscyglem4  42194  aks5lem8  42197  infdesc  42646  pellfundex  42890  monotoddzzfi  42947  jm2.23  43001  rp-isfinite6  43524  r1rankcld  44243  iccpartiltu  47375  iccpartigtl  47376