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

Theorem pm2.21i 613
Description: A contradiction implies anything. Inference from pm2.21 585. (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 585 . 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 583
This theorem is referenced by:  pm2.24ii  614  2false  655  pm3.2ni  765  falim  1310  pclem6  1317  nfnth  1406  alnex  1440  ax4sp1  1478  rex0  3319  0ss  3340  abf  3345  ral0  3403  int0  3724  nnsucelsuc  6292  nnmordi  6315  nnaordex  6326  0er  6366  fiintim  6719  elnnnn0b  8815  xltnegi  9401  xnn0xadd0  9433  frec2uzltd  9959  sum0  10947  fsum2dlemstep  10993  nn0enne  11345  exprmfct  11562  0met  12186
  Copyright terms: Public domain W3C validator