New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > con3d | Unicode version |
Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
con3d.1 |
Ref | Expression |
---|---|
con3d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot2 104 | . . 3 | |
2 | con3d.1 | . . 3 | |
3 | 1, 2 | syl5 28 | . 2 |
4 | 3 | con1d 116 | 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: con3 126 con3rr3 128 nsyld 132 nsyli 133 mth8 138 pm2.52 147 pm5.21ndd 343 bija 344 con3and 428 ax12bOLD 1690 ax12olem1 1927 spime 1976 mo 2226 necon1bd 2584 rexim 2718 spcimegf 2933 spcimedv 2938 rspcimedv 2957 ssneld 3275 sscon 3400 difrab 3529 ssofss 4076 pwadjoin 4119 nnsucelrlem2 4425 nnadjoin 4520 sfinltfin 4535 vfinspsslem1 4550 phi11lem1 4595 phialllem1 4616 eqfnfv 5392 dff3 5420 ndmovg 5613 nchoicelem3 6291 |
Copyright terms: Public domain | W3C validator |