Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > con3d | Unicode version |
Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
con3d.1 |
Ref | Expression |
---|---|
con3d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con3d.1 | . . 3 | |
2 | notnot 559 | . . 3 | |
3 | 1, 2 | syl6 29 | . 2 |
4 | 3 | con2d 554 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 544 ax-in2 545 |
This theorem is referenced by: con3rr3 563 con3and 564 con3 571 nsyld 577 nsyli 578 mth8 579 notbid 592 impidc 755 bijadc 776 pm2.13dc 779 xoranor 1268 mo2n 1928 necon3ad 2247 necon3bd 2248 ssneld 2947 sscon 3077 difrab 3211 eunex 4285 ndmfvg 5204 nnaord 6082 nnmord 6090 php5 6321 php5dom 6325 prubl 6584 letr 7101 prodge0 7820 lt2msq 7852 nnge1 7937 irradd 8580 irrmul 8581 xrletr 8724 frec2uzf1od 9192 zesq 9367 bj-notbi 10045 bj-nnelirr 10078 |
Copyright terms: Public domain | W3C validator |