![]() |
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 601 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6 33 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con2d 596 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 586 ax-in2 587 |
This theorem is referenced by: con3rr3 605 con3dimp 607 con3 614 nsyld 620 nsyli 621 mth8 622 notbi 638 impidc 826 bijadc 850 pm2.13dc 853 xoranor 1338 mo2n 2003 necon3ad 2324 necon3bd 2325 nelcon3d 2388 ssneld 3065 sscon 3176 difrab 3316 eunex 4436 ndmfvg 5406 nnaord 6359 nnmord 6367 php5 6705 php5dom 6710 supmoti 6832 exmidomniim 6963 mkvprop 6982 prubl 7242 letr 7770 eqord1 8164 cnstab 8324 prodge0 8522 lt2msq 8554 nnge1 8653 nzadd 9010 irradd 9340 irrmul 9341 xrletr 9484 frec2uzf1od 10072 zesq 10303 expcanlem 10355 nn0opthd 10361 bccmpl 10393 maxleast 10877 fisumss 11053 efler 11256 dvdsbnd 11493 prm2orodd 11653 coprm 11668 prmndvdsfaclt 11680 hashgcdeq 11749 bj-nnsn 12638 bj-nnelirr 12843 exmid1stab 12887 |
Copyright terms: Public domain | W3C validator |