![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imbitrdi | Unicode version |
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbitrdi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
imbitrdi.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imbitrdi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbitrdi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | imbitrdi.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | biimpi 120 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl6 33 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3imtr3g 204 exp4a 366 con2biddc 881 nfalt 1588 alexim 1655 19.36-1 1683 ax11ev 1838 equs5or 1840 necon2bd 2415 necon2d 2416 necon1bbiddc 2420 necon2abiddc 2423 necon2bbiddc 2424 necon4idc 2426 necon4ddc 2429 necon1bddc 2434 spc2gv 2840 spc3gv 2842 mo2icl 2928 reupick 3431 prneimg 3786 invdisj 4009 trin 4123 exmidsssnc 4215 ordsucss 4515 eqbrrdva 4809 elreldm 4865 elres 4955 xp11m 5079 ssrnres 5083 opelf 5399 dffo4 5677 dftpos3 6277 tfr1onlemaccex 6363 tfrcllemaccex 6376 nnaordex 6543 swoer 6577 map0g 6702 mapsn 6704 nneneq 6871 fnfi 6950 prarloclemlo 7507 genprndl 7534 genprndu 7535 cauappcvgprlemladdrl 7670 caucvgprlemladdrl 7691 caucvgsrlemoffres 7813 caucvgsr 7815 nntopi 7907 letr 8054 reapcotr 8569 apcotr 8578 mulext1 8583 lt2msq 8857 nneoor 9369 xrletr 9822 icoshft 10004 caucvgre 11004 absext 11086 rexico 11244 summodc 11405 gcdeq0 11992 intopsn 12805 tgcn 14061 cnptoprest 14092 metequiv2 14349 bj-nnsn 14838 bj-inf2vnlem2 15076 |
Copyright terms: Public domain | W3C validator |