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  1562  pm2.21ddne  3009  smo11  8333  ackbij1lem16  10187  cfsmolem  10223  domtriomlem  10395  konigthlem  10521  grur1  10773  uzdisj  13558  nn0disj  13605  psgnunilem2  19425  nmoleub2lem3  25015  i1f0  25588  itg2const2  25642  bposlem3  27197  bposlem9  27203  pntpbnd1  27497  sgnmul  32760  sgnmulsgn  32767  sgnmulsgp  32768  ccatf1  32870  chnccats1  32941  fzto1st1  33059  cycpmco2lem5  33087  mxidlirred  33443  rprmdvdspow  33504  1arithufd  33519  esumpcvgval  34068  signstfvneq0  34563  derangsn  35157  heiborlem8  37812  lkrpssN  39156  cdleme27a  40361  aks4d1p3  42066  aks4d1p5  42068  aks4d1p8  42075  primrootlekpowne0  42093  primrootspoweq0  42094  sticksstones22  42156  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c7lem2  42169  unitscyglem2  42184  unitscyglem4  42186  aks5lem8  42189  infdesc  42631  pellfundex  42874  monotoddzzfi  42931  jm2.23  42985  rp-isfinite6  43507  r1rankcld  44220  iccpartiltu  47423  iccpartigtl  47424  pgn4cyclex  48116