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

Theorem pm2.21i 574
Description: A contradiction implies anything. Inference from pm2.21 547. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
pm2.21i.1 ¬ φ
Assertion
Ref Expression
pm2.21i (φψ)

Proof of Theorem pm2.21i
StepHypRef Expression
1 pm2.21i.1 . 2 ¬ φ
2 pm2.21 547 . 2 φ → (φψ))
31, 2ax-mp 7 1 (φψ)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 7  ax-in2 545
This theorem is referenced by:  pm2.24ii  575  2false  616  pm3.2ni  725  falim  1256  pclem6  1264  nfnth  1351  alnex  1385  ax4sp1  1423  rex0  3232  0ss  3249  abf  3254  ral0  3316  int0  3620  nnsucelsuc  6009  nnmordi  6025  nnaordex  6036  0er  6076  elnnnn0b  7962  xltnegi  8478  frec2uzltd  8830
  Copyright terms: Public domain W3C validator