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

Theorem pm2.21i 635
Description: A contradiction implies anything. Inference from pm2.21 606. (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 606 . 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 604
This theorem is referenced by:  pm2.24ii  636  2false  690  pm3.2ni  802  falim  1345  pclem6  1352  nfnth  1441  alnex  1475  ax4sp1  1513  rex0  3380  0ss  3401  abf  3406  ral0  3464  int0  3785  nnsucelsuc  6387  nnmordi  6412  nnaordex  6423  0er  6463  fiintim  6817  elnnnn0b  9028  xltnegi  9625  xnn0xadd0  9657  frec2uzltd  10183  sum0  11164  fsum2dlemstep  11210  nn0enne  11606  exprmfct  11825  0met  12563
  Copyright terms: Public domain W3C validator