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

Theorem pm2.21dd 177
Description: A contradiction implies anything. Deduction from pm2.21 111. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.)
Hypotheses
Ref Expression
pm2.21dd.1  |-  ( ph  ->  ps )
pm2.21dd.2  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
pm2.21dd  |-  ( ph  ->  ch )

Proof of Theorem pm2.21dd
StepHypRef Expression
1 pm2.21dd.1 . . 3  |-  ( ph  ->  ps )
2 pm2.21dd.2 . . 3  |-  ( ph  ->  -.  ps )
31, 2pm2.65i 176 . 2  |-  -.  ph
43pm2.21i 134 1  |-  ( ph  ->  ch )
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  1460  pm2.21ddne  2745  smo11  7091  ackbij1lem16  8663  cfsmolem  8698  domtriomlem  8870  konigthlem  8991  grur1  9244  uzdisj  11865  nn0disj  11905  psgnunilem2  17087  nmoleub2lem3  22022  i1f0  22522  itg2const2  22576  bposlem3  24077  bposlem9  24083  pntpbnd1  24287  fzto1st1  28454  esumpcvgval  28738  sgnmul  29201  sgnmulsgn  29208  sgnmulsgp  29209  signstfvneq0  29249  derangsn  29681  heiborlem8  31854  lkrpssN  32438  cdleme27a  33643  pellfundex  35440  monotoddzzfi  35496  jm2.23  35557  rp-isfinite6  35862  iccpartiltu  38126  iccpartigtl  38127
  Copyright terms: Public domain W3C validator