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  1564  pm2.21ddne  3017  smo11  8297  ackbij1lem16  10147  cfsmolem  10183  domtriomlem  10355  konigthlem  10482  grur1  10734  uzdisj  13542  nn0disj  13589  chnccats1  18582  chnccat  18583  psgnunilem2  19461  nmoleub2lem3  25092  i1f0  25664  itg2const2  25718  bposlem3  27263  bposlem9  27269  pntpbnd1  27563  sgnmul  32923  sgnmulsgn  32930  sgnmulsgp  32931  ccatf1  33024  fzto1st1  33178  cycpmco2lem5  33206  mxidlirred  33547  rprmdvdspow  33608  1arithufd  33623  esumpcvgval  34238  signstfvneq0  34732  derangsn  35368  heiborlem8  38153  lkrpssN  39623  cdleme27a  40827  aks4d1p3  42531  aks4d1p5  42533  aks4d1p8  42540  primrootlekpowne0  42558  primrootspoweq0  42559  sticksstones22  42621  aks6d1c6lem3  42625  aks6d1c6lem4  42626  aks6d1c7lem2  42634  unitscyglem2  42649  unitscyglem4  42651  aks5lem8  42654  infdesc  43090  pellfundex  43332  monotoddzzfi  43388  jm2.23  43442  rp-isfinite6  43963  r1rankcld  44676  iccpartiltu  47894  iccpartigtl  47895  pgn4cyclex  48614