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

Theorem pm2.21dd 174
Description: A contradiction implies anything. Deduction from pm2.21 108. (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 173 . 2  |-  -.  ph
43pm2.21i 131 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  1387  pm2.21ddne  2683  smo11  6821  ackbij1lem16  8400  cfsmolem  8435  domtriomlem  8607  konigthlem  8728  grur1  8983  uzdisj  11527  psgnunilem2  15994  nmoleub2lem3  20570  i1f0  21065  itg2const2  21119  bposlem3  22568  bposlem9  22574  pntpbnd1  22778  archiabllem2c  26129  esumpcvgval  26447  sgnmul  26839  sgnsub  26841  sgnmulsgn  26846  sgnmulsgp  26847  signstfvneq0  26887  derangsn  26972  heiborlem8  28626  negel  28817  pellfundex  29136  monotoddzzfi  29192  jm2.23  29254  lkrpssN  32496  cdleme27a  33699
  Copyright terms: Public domain W3C validator