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

Theorem pm2.21i 575
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  576  2false  617  pm3.2ni  726  falim  1257  pclem6  1265  nfnth  1354  alnex  1388  ax4sp1  1426  rex0  3235  0ss  3252  abf  3257  ral0  3319  int0  3626  nnsucelsuc  6057  nnmordi  6076  nnaordex  6087  0er  6127  elnnnn0b  8198  xltnegi  8715  frec2uzltd  9067
  Copyright terms: Public domain W3C validator