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

Theorem pm2.21i 608
Description: A contradiction implies anything. Inference from pm2.21 580. (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 580 . 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 578
This theorem is referenced by:  pm2.24ii  609  2false  650  pm3.2ni  760  falim  1299  pclem6  1306  nfnth  1395  alnex  1429  ax4sp1  1467  rex0  3283  0ss  3303  abf  3308  ral0  3364  int0  3676  nnsucelsuc  6184  nnmordi  6205  nnaordex  6216  0er  6256  elnnnn0b  8609  xltnegi  9192  frec2uzltd  9699  nn0enne  10682  exprmfct  10899
  Copyright terms: Public domain W3C validator