New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > pm2.21i | GIF version |
Description: A contradiction implies anything. Inference from pm2.21 100. (Contributed by NM, 16-Sep-1993.) |
Ref | Expression |
---|---|
pm2.21i.1 | ⊢ ¬ φ |
Ref | Expression |
---|---|
pm2.21i | ⊢ (φ → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21i.1 | . . 3 ⊢ ¬ φ | |
2 | 1 | a1i 10 | . 2 ⊢ (¬ ψ → ¬ φ) |
3 | 2 | con4i 122 | 1 ⊢ (φ → ψ) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: pm2.24ii 124 pm3.2ni 827 falim 1328 nfnth 1556 ax4sp1 2174 rex0 3563 0ss 3579 abf 3584 r19.2zb 3640 ral0 3654 snsssn 3873 int0 3940 clos10 5887 po0 5939 connex0 5940 fnfreclem2 6318 fnfreclem3 6319 |
Copyright terms: Public domain | W3C validator |