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

Theorem pm2.21i 620
Description: A contradiction implies anything. Inference from pm2.21 591. (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 591 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2ax-mp 5 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-in2 589
This theorem is referenced by:  pm2.24ii  621  2false  675  pm3.2ni  787  falim  1330  pclem6  1337  nfnth  1426  alnex  1460  ax4sp1  1498  rex0  3350  0ss  3371  abf  3376  ral0  3434  int0  3755  nnsucelsuc  6355  nnmordi  6380  nnaordex  6391  0er  6431  fiintim  6785  elnnnn0b  8989  xltnegi  9586  xnn0xadd0  9618  frec2uzltd  10144  sum0  11125  fsum2dlemstep  11171  nn0enne  11526  exprmfct  11745  0met  12480
  Copyright terms: Public domain W3C validator