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

Theorem pm2.21i 585
Description: A contradiction implies anything. Inference from pm2.21 557. (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 557 . 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 555
This theorem is referenced by:  pm2.24ii  586  2false  627  pm3.2ni  737  falim  1273  pclem6  1281  nfnth  1370  alnex  1404  ax4sp1  1442  rex0  3265  0ss  3282  abf  3287  ral0  3349  int0  3656  nnsucelsuc  6100  nnmordi  6119  nnaordex  6130  0er  6170  elnnnn0b  8282  xltnegi  8848  frec2uzltd  9352  nn0enne  10213
  Copyright terms: Public domain W3C validator