Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm2.21i | GIF version |
Description: A contradiction implies anything. Inference from pm2.21 606. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
pm2.21i.1 | ⊢ ¬ 𝜑 |
Ref | Expression |
---|---|
pm2.21i | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21i.1 | . 2 ⊢ ¬ 𝜑 | |
2 | pm2.21 606 | . 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
3 | 1, 2 | ax-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 3380 0ss 3401 abf 3406 ral0 3464 int0 3785 nnsucelsuc 6387 nnmordi 6412 nnaordex 6423 0er 6463 fiintim 6817 elnnnn0b 9021 xltnegi 9618 xnn0xadd0 9650 frec2uzltd 10176 sum0 11157 fsum2dlemstep 11203 nn0enne 11599 exprmfct 11818 0met 12553 |
Copyright terms: Public domain | W3C validator |