MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21dd Structured version   Visualization version   GIF version

Theorem pm2.21dd 185
Description: A contradiction implies anything. Deduction from pm2.21 119. (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
StepHypRef Expression
1 pm2.21dd.1 . . 3 (𝜑𝜓)
2 pm2.21dd.2 . . 3 (𝜑 → ¬ 𝜓)
31, 2pm2.65i 184 . 2 ¬ 𝜑
43pm2.21i 115 1 (𝜑𝜒)
Colors of variables: wff setvar class
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  1496  pm2.21ddne  2866  smo11  7348  ackbij1lem16  8940  cfsmolem  8975  domtriomlem  9147  konigthlem  9269  grur1  9521  uzdisj  12282  nn0disj  12324  psgnunilem2  17738  nmoleub2lem3  22723  i1f0  23260  itg2const2  23314  bposlem3  24811  bposlem9  24817  pntpbnd1  25075  fzto1st1  29183  esumpcvgval  29467  sgnmul  29931  sgnmulsgn  29938  sgnmulsgp  29939  signstfvneq0  29975  derangsn  30406  heiborlem8  32787  lkrpssN  33468  cdleme27a  34673  pellfundex  36468  monotoddzzfi  36525  jm2.23  36581  rp-isfinite6  36883  iccpartiltu  39960  iccpartigtl  39961
  Copyright terms: Public domain W3C validator