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 187
Description: A contradiction implies anything. Deduction from pm2.21 121. (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 186 . 2 ¬ 𝜑
43pm2.21i 117 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  1679  pm2.21ddne  3083  smo11  7727  ackbij1lem16  9372  cfsmolem  9407  domtriomlem  9579  konigthlem  9705  grur1  9957  uzdisj  12707  nn0disj  12750  psgnunilem2  18266  nmoleub2lem3  23284  i1f0  23853  itg2const2  23907  bposlem3  25424  bposlem9  25430  pntpbnd1  25688  fzto1st1  30386  esumpcvgval  30674  sgnmul  31139  sgnmulsgn  31146  sgnmulsgp  31147  signstfvneq0  31186  derangsn  31687  heiborlem8  34152  lkrpssN  35231  cdleme27a  36435  pellfundex  38287  monotoddzzfi  38343  jm2.23  38399  rp-isfinite6  38698  iccpartiltu  42239  iccpartigtl  42240
  Copyright terms: Public domain W3C validator