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 603 | . . 3 | |
3 | 1, 2 | syl6 33 | . 2 |
4 | 3 | con2d 598 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 588 ax-in2 589 |
This theorem is referenced by: con3rr3 607 con3dimp 609 con3 616 nsyld 622 nsyli 623 mth8 624 notbi 640 impidc 828 bijadc 852 pm2.13dc 855 xoranor 1340 mo2n 2005 necon3ad 2327 necon3bd 2328 nelcon3d 2391 ssneld 3069 sscon 3180 difrab 3320 eunex 4446 ndmfvg 5420 nnaord 6373 nnmord 6381 php5 6720 php5dom 6725 supmoti 6848 exmidomniim 6981 mkvprop 7000 prubl 7262 letr 7815 eqord1 8213 cnstab 8375 prodge0 8580 lt2msq 8612 nnge1 8711 nzadd 9074 irradd 9406 irrmul 9407 xrletr 9559 frec2uzf1od 10147 zesq 10378 expcanlem 10430 nn0opthd 10436 bccmpl 10468 maxleast 10953 fisumss 11129 efler 11332 dvdsbnd 11572 prm2orodd 11734 coprm 11749 prmndvdsfaclt 11761 hashgcdeq 11831 bj-nnsn 12872 bj-nnelirr 13078 exmid1stab 13122 |
Copyright terms: Public domain | W3C validator |