![]() |
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 594 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6 33 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con2d 589 |
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 579 ax-in2 580 |
This theorem is referenced by: con3rr3 598 con3dimp 599 con3 606 nsyld 612 nsyli 613 mth8 614 notbid 627 impidc 793 bijadc 814 pm2.13dc 817 xoranor 1313 mo2n 1976 necon3ad 2297 necon3bd 2298 ssneld 3027 sscon 3134 difrab 3273 eunex 4377 ndmfvg 5335 nnaord 6266 nnmord 6274 php5 6572 php5dom 6577 supmoti 6686 exmidomniim 6795 prubl 7043 letr 7566 eqord1 7959 prodge0 8313 lt2msq 8345 nnge1 8443 nzadd 8800 irradd 9129 irrmul 9130 xrletr 9271 frec2uzf1od 9809 zesq 10068 expcanlem 10120 nn0opthd 10126 bccmpl 10158 maxleast 10642 fisumss 10780 efler 10985 dvdsbnd 11222 prm2orodd 11382 coprm 11397 prmndvdsfaclt 11409 hashgcdeq 11478 bj-notbi 11771 bj-nnelirr 11803 |
Copyright terms: Public domain | W3C validator |