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

Theorem pm2.21i 585
Description: A contradiction implies anything. Inference from pm2.21 557. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
pm2.21i.1  |-  -.  ph
Assertion
Ref Expression
pm2.21i  |-  ( ph  ->  ps )

Proof of Theorem pm2.21i
StepHypRef Expression
1 pm2.21i.1 . 2  |-  -.  ph
2 pm2.21 557 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2ax-mp 7 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 7  ax-in2 555
This theorem is referenced by:  pm2.24ii  586  2false  627  pm3.2ni  737  falim  1273  pclem6  1281  nfnth  1370  alnex  1404  ax4sp1  1442  rex0  3266  0ss  3283  abf  3288  ral0  3350  int0  3657  nnsucelsuc  6101  nnmordi  6120  nnaordex  6131  0er  6171  elnnnn0b  8283  xltnegi  8849  frec2uzltd  9353  nn0enne  10214
  Copyright terms: Public domain W3C validator