ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.21dd Unicode version

Theorem pm2.21dd 560
Description: A contradiction implies anything. Deduction from pm2.21 557. (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 559 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in2 555
This theorem is referenced by:  pm2.21fal  1280  pm2.21ddne  2303  ordtriexmidlem  4273  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  wetriext  4329  reg3exmidlemwe  4331  nnm00  6133  phpm  6358  fidifsnen  6362  aptiprleml  6795  aptiprlemu  6796  uzdisj  9057  nn0disj  9097  addmodlteq  9348  frec2uzlt2d  9354  divalglemeunn  10233  divalglemeuneg  10235
  Copyright terms: Public domain W3C validator