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

Theorem pm2.21i 636
Description: A contradiction implies anything. Inference from pm2.21 607. (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 607 . 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 605
This theorem is referenced by:  pm2.24ii  637  2false  691  pm3.2ni  803  falim  1349  pclem6  1356  nfnth  1445  alnex  1479  ax4sp1  1513  rex0  3412  0ss  3433  abf  3438  ral0  3496  int0  3823  nnsucelsuc  6440  nnmordi  6465  nnaordex  6476  0er  6516  fiintim  6875  elnnnn0b  9139  xltnegi  9745  xnn0xadd0  9777  frec2uzltd  10311  sum0  11296  fsum2dlemstep  11342  prod0  11493  fprod2dlemstep  11530  nn0enne  11805  exprmfct  12030  prm23lt5  12153  0met  12854
  Copyright terms: Public domain W3C validator