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

Theorem pm2.21dd 101
Description: A contradiction implies anything. Deduction from pm2.21 102. (Contributed by Mario Carneiro, 9-Feb-2017.)
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 . 2  |-  ( ph  ->  ps )
2 pm2.21dd.2 . . 3  |-  ( ph  ->  -.  ps )
32pm2.21d 100 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21fal  1341  pm2.21ddne  2641  smo11  6585  ackbij1lem16  8071  cfsmolem  8106  domtriomlem  8278  konigthlem  8399  grur1  8651  uzdisj  11074  nmoleub2lem3  19076  i1f0  19532  itg2const2  19586  bposlem3  21023  bposlem9  21029  pntpbnd1  21233  esumpcvgval  24421  derangsn  24809  heiborlem8  26417  pellfundex  26839  monotoddzzfi  26895  jm2.23  26957  psgnunilem2  27286  lkrpssN  29646  cdleme27a  30849
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator