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 363 con2biddc 850 nfalt 1542 alexim 1609 19.36-1 1636 ax11ev 1784 equs5or 1786 necon2bd 2343 necon2d 2344 necon1bbiddc 2348 necon2abiddc 2351 necon2bbiddc 2352 necon4idc 2354 necon4ddc 2357 necon1bddc 2362 spc2gv 2750 spc3gv 2752 mo2icl 2836 reupick 3330 prneimg 3671 invdisj 3893 trin 4006 exmidsssnc 4096 ordsucss 4390 eqbrrdva 4679 elreldm 4735 elres 4825 xp11m 4947 ssrnres 4951 opelf 5264 dffo4 5536 dftpos3 6127 tfr1onlemaccex 6213 tfrcllemaccex 6226 nnaordex 6391 swoer 6425 map0g 6550 mapsn 6552 nneneq 6719 fnfi 6793 prarloclemlo 7270 genprndl 7297 genprndu 7298 cauappcvgprlemladdrl 7433 caucvgprlemladdrl 7454 caucvgsrlemoffres 7576 caucvgsr 7578 nntopi 7670 letr 7815 reapcotr 8328 apcotr 8337 mulext1 8342 cnstab 8375 lt2msq 8612 nneoor 9121 xrletr 9559 icoshft 9741 caucvgre 10721 absext 10803 rexico 10961 summodc 11120 gcdeq0 11592 tgcn 12304 cnptoprest 12335 metequiv2 12592 bj-nnsn 12872 bj-inf2vnlem2 13096 |
Copyright terms: Public domain | W3C validator |