![]() |
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 629 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6 33 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con2d 624 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 614 ax-in2 615 |
This theorem is referenced by: con3rr3 633 con3dimp 635 con3 642 nsyld 648 nsyli 649 jcn 651 notbi 666 impidc 858 bijadc 882 pm2.13dc 885 xoranor 1377 mo2n 2054 necon3ad 2389 necon3bd 2390 nelcon3d 2453 ssneld 3157 sscon 3269 difrab 3409 exmid1stab 4208 eunex 4560 ndmfvg 5546 nnaord 6509 nnmord 6517 php5 6857 php5dom 6862 supmoti 6991 exmidomniim 7138 mkvprop 7155 enmkvlem 7158 prubl 7484 letr 8038 eqord1 8438 prodge0 8809 lt2msq 8841 nnge1 8940 nzadd 9303 irradd 9644 irrmul 9645 xrletr 9806 frec2uzf1od 10403 zesq 10635 expcanlem 10690 nn0opthd 10697 bccmpl 10729 maxleast 11217 fisumss 11395 dvdsbnd 11951 prm2orodd 12120 coprm 12138 prmndvdsfaclt 12150 hashgcdeq 12233 cos11 14167 bj-nnsn 14367 bj-nnelirr 14587 ismkvnnlem 14682 nconstwlpolem 14694 |
Copyright terms: Public domain | W3C validator |