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 618 | 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: notnotnot 624 conax1 643 pm5.21ni 693 pm2.45 728 pm2.46 729 pm3.14 743 3ianorr 1298 nalequcoms 1504 equidqe 1519 nnal 1636 ax6blem 1637 hbnt 1640 naecoms 1711 euor2 2071 moexexdc 2097 baroco 2120 necon3ai 2383 necon3bi 2384 nnral 2454 eueq3dc 2895 difin 3354 indifdir 3373 difrab 3391 csbprc 3449 ifandc 3551 nelpri 3594 nelprd 3596 opprc 3773 opprc1 3774 opprc2 3775 notnotsnex 4160 eldifpw 4449 nlimsucg 4537 nfvres 5513 nfunsn 5514 ressnop0 5660 ovprc 5868 ovprc1 5869 ovprc2 5870 mapprc 6609 ixpprc 6676 ixp0 6688 fiprc 6772 fidceq 6826 unfiexmid 6874 difinfsnlem 7055 3nsssucpw1 7183 onntri51 7187 onntri52 7191 fzdcel 9965 bcpasc 10668 flodddiv4lt 11858 bj-nnan 13460 bj-nnst 13479 nnnotnotr 13713 nninfsellemsuc 13733 |
Copyright terms: Public domain | W3C validator |