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  1392  pm2.21ddne  2685  smo11  6825  ackbij1lem16  8404  cfsmolem  8439  domtriomlem  8611  konigthlem  8732  grur1  8987  uzdisj  11531  psgnunilem2  16001  nmoleub2lem3  20670  i1f0  21165  itg2const2  21219  bposlem3  22625  bposlem9  22631  pntpbnd1  22835  archiabllem2c  26212  esumpcvgval  26527  sgnmul  26925  sgnsub  26927  sgnmulsgn  26932  sgnmulsgp  26933  signstfvneq0  26973  derangsn  27058  heiborlem8  28717  negel  28908  pellfundex  29227  monotoddzzfi  29283  jm2.23  29345  lkrpssN  32808  cdleme27a  34011
  Copyright terms: Public domain W3C validator