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

Theorem pm2.21i 610
Description: A contradiction implies anything. Inference from pm2.21 582. (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 582 . 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 580
This theorem is referenced by:  pm2.24ii  611  2false  652  pm3.2ni  762  falim  1303  pclem6  1310  nfnth  1399  alnex  1433  ax4sp1  1471  rex0  3298  0ss  3318  abf  3323  ral0  3379  int0  3697  nnsucelsuc  6234  nnmordi  6255  nnaordex  6266  0er  6306  elnnnn0b  8687  xltnegi  9266  frec2uzltd  9775  sum0  10744  fsum2dlemstep  10791  nn0enne  10984  exprmfct  11201
  Copyright terms: Public domain W3C validator