Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6ib | Unicode version |
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6ib.1 | |
syl6ib.2 |
Ref | Expression |
---|---|
syl6ib |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6ib.1 | . 2 | |
2 | syl6ib.2 | . . 3 | |
3 | 2 | biimpi 119 | . 2 |
4 | 1, 3 | syl6 33 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3imtr3g 203 exp4a 364 con2biddc 870 nfalt 1565 alexim 1632 19.36-1 1660 ax11ev 1815 equs5or 1817 necon2bd 2392 necon2d 2393 necon1bbiddc 2397 necon2abiddc 2400 necon2bbiddc 2401 necon4idc 2403 necon4ddc 2406 necon1bddc 2411 spc2gv 2815 spc3gv 2817 mo2icl 2903 reupick 3404 prneimg 3751 invdisj 3973 trin 4087 exmidsssnc 4179 ordsucss 4478 eqbrrdva 4771 elreldm 4827 elres 4917 xp11m 5039 ssrnres 5043 opelf 5356 dffo4 5630 dftpos3 6224 tfr1onlemaccex 6310 tfrcllemaccex 6323 nnaordex 6489 swoer 6523 map0g 6648 mapsn 6650 nneneq 6817 fnfi 6896 prarloclemlo 7429 genprndl 7456 genprndu 7457 cauappcvgprlemladdrl 7592 caucvgprlemladdrl 7613 caucvgsrlemoffres 7735 caucvgsr 7737 nntopi 7829 letr 7975 reapcotr 8490 apcotr 8499 mulext1 8504 lt2msq 8775 nneoor 9287 xrletr 9738 icoshft 9920 caucvgre 10917 absext 10999 rexico 11157 summodc 11318 gcdeq0 11904 tgcn 12806 cnptoprest 12837 metequiv2 13094 bj-nnsn 13508 bj-inf2vnlem2 13746 |
Copyright terms: Public domain | W3C validator |