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 619 | . . 3 | |
3 | 1, 2 | syl6 33 | . 2 |
4 | 3 | con2d 614 | 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 604 ax-in2 605 |
This theorem is referenced by: con3rr3 623 con3dimp 625 con3 632 nsyld 638 nsyli 639 jcn 641 notbi 656 impidc 848 bijadc 872 pm2.13dc 875 xoranor 1366 mo2n 2041 necon3ad 2376 necon3bd 2377 nelcon3d 2440 ssneld 3139 sscon 3251 difrab 3391 eunex 4532 ndmfvg 5511 nnaord 6468 nnmord 6476 php5 6815 php5dom 6820 supmoti 6949 exmidomniim 7096 mkvprop 7113 enmkvlem 7116 prubl 7418 letr 7972 eqord1 8372 prodge0 8740 lt2msq 8772 nnge1 8871 nzadd 9234 irradd 9575 irrmul 9576 xrletr 9735 frec2uzf1od 10331 zesq 10562 expcanlem 10617 nn0opthd 10624 bccmpl 10656 maxleast 11141 fisumss 11319 dvdsbnd 11874 prm2orodd 12037 coprm 12055 prmndvdsfaclt 12067 hashgcdeq 12150 cos11 13321 bj-nnsn 13457 bj-nnelirr 13676 exmid1stab 13721 ismkvnnlem 13772 nconstwlpolem 13784 |
Copyright terms: Public domain | W3C validator |