![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > con3i | Unicode version |
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.) |
Ref | Expression |
---|---|
con3i.a |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
con3i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | con3i.a |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | nsyl 558 |
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 544 ax-in2 545 |
This theorem is referenced by: pm2.51 580 pm5.21ni 618 notnotnot 627 pm2.45 656 pm2.46 657 pm3.14 669 3ianorr 1203 nalequcoms 1407 equidqe 1422 ax6blem 1537 hbnt 1540 naecoms 1609 euor2 1955 moexexdc 1981 baroco 2004 necon3ai 2248 necon3bi 2249 eueq3dc 2709 difin 3168 indifdir 3187 difrab 3205 csbprc 3256 nelpri 3388 opprc 3561 opprc1 3562 opprc2 3563 eldifpw 4174 nlimsucg 4242 nfvres 5149 nfunsn 5150 ressnop0 5287 ovprc 5482 ovprc1 5483 ovprc2 5484 fiprc 6228 fzdcel 8674 |
Copyright terms: Public domain | W3C validator |