Theorem pm2.21dd 186

Description: A contradiction implies anything. Deduction from pm2.21 120. (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 185	. 2 ⊢ ¬ 𝜑
4	3	pm2.21i 116	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  1505  pm2.21ddne  2878  smo11  7461  ackbij1lem16  9057  cfsmolem  9092  domtriomlem  9264  konigthlem  9390  grur1  9642  uzdisj  12413  nn0disj  12455  psgnunilem2  17915  nmoleub2lem3  22915  i1f0  23454  itg2const2  23508  bposlem3  25011  bposlem9  25017  pntpbnd1  25275  fzto1st1  29852  esumpcvgval  30140  sgnmul  30604  sgnmulsgn  30611  sgnmulsgp  30612  signstfvneq0  30649  derangsn  31152  heiborlem8  33617  lkrpssN  34450  cdleme27a  35655  pellfundex  37450  monotoddzzfi  37507  jm2.23  37563  rp-isfinite6  37864  iccpartiltu  41358  iccpartigtl  41359