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

Theorem pm2.21i 562
Description: A contradiction implies anything. Inference from pm2.21 535. (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 535 . 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 533
This theorem is referenced by:  pm2.24ii  563  2false  604  pm3.2ni  713  falim  1242  pclem6  1250  nfnth  1334  alnex  1369  ax4sp1  1408  rex0  3215  0ss  3232  abf  3237  ral0  3301  int0  3603  nnsucelsuc  5985  nnmordi  6000  nnaordex  6011  0er  6051
  Copyright terms: Public domain W3C validator