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

Theorem pm2.21i 641
Description: A contradiction implies anything. Inference from pm2.21 612. (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 612 . 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 610
This theorem is referenced by:  pm2.24ii  642  2false  696  pm3.2ni  808  falim  1362  pclem6  1369  nfnth  1458  alnex  1492  ax4sp1  1526  rex0  3432  0ss  3453  abf  3458  ral0  3516  int0  3845  nnsucelsuc  6470  nnmordi  6495  nnaordex  6507  0er  6547  fiintim  6906  elnnnn0b  9179  xltnegi  9792  xnn0xadd0  9824  frec2uzltd  10359  sum0  11351  fsum2dlemstep  11397  prod0  11548  fprod2dlemstep  11585  nn0enne  11861  exprmfct  12092  prm23lt5  12217  0met  13178  lgsdir2lem3  13725
  Copyright terms: Public domain W3C validator