ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.21i GIF 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 ¬ 𝜑
Assertion
Ref Expression
pm2.21i (𝜑𝜓)

Proof of Theorem pm2.21i
StepHypRef Expression
1 pm2.21i.1 . 2 ¬ 𝜑
2 pm2.21 606 . 2 𝜑 → (𝜑𝜓))
31, 2ax-mp 5 1 (𝜑𝜓)
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  3375  0ss  3396  abf  3401  ral0  3459  int0  3780  nnsucelsuc  6380  nnmordi  6405  nnaordex  6416  0er  6456  fiintim  6810  elnnnn0b  9014  xltnegi  9611  xnn0xadd0  9643  frec2uzltd  10169  sum0  11150  fsum2dlemstep  11196  nn0enne  11588  exprmfct  11807  0met  12542
  Copyright terms: Public domain W3C validator