New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > con2d | Unicode version |
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.) |
Ref | Expression |
---|---|
con2d.1 |
Ref | Expression |
---|---|
con2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot2 104 | . . 3 | |
2 | con2d.1 | . . 3 | |
3 | 1, 2 | syl5 28 | . 2 |
4 | 3 | con4d 97 | 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: con2 108 mt2d 109 pm3.2im 137 exists2 2294 necon3ad 2552 necon2bd 2565 necon4ad 2577 spcimegf 2933 spcegf 2935 spcimedv 2938 rspcimedv 2957 minel 3606 tfinltfin 4501 tfinnn 4534 imadif 5171 nchoicelem14 6302 |
Copyright terms: Public domain | W3C validator |