Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3imtr4g | Unicode version |
Description: More general version of 3imtr4i 200. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
Ref | Expression |
---|---|
3imtr4g.1 | |
3imtr4g.2 | |
3imtr4g.3 |
Ref | Expression |
---|---|
3imtr4g |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imtr4g.2 | . . 3 | |
2 | 3imtr4g.1 | . . 3 | |
3 | 1, 2 | syl5bi 151 | . 2 |
4 | 3imtr4g.3 | . 2 | |
5 | 3, 4 | syl6ibr 161 | 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 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3anim123d 1297 3orim123d 1298 hbbid 1554 spsbim 1815 moim 2063 moimv 2065 2euswapdc 2090 nelcon3d 2414 ralim 2491 ralimdaa 2498 ralimdv2 2502 rexim 2526 reximdv2 2531 rmoim 2885 ssel 3091 sstr2 3104 ssrexf 3159 ssrmof 3160 sscon 3210 ssdif 3211 unss1 3245 ssrin 3301 prel12 3698 uniss 3757 ssuni 3758 intss 3792 intssunim 3793 iunss1 3824 iinss1 3825 ss2iun 3828 disjss2 3909 disjss1 3912 ssbrd 3971 sspwb 4138 poss 4220 pofun 4234 soss 4236 sess1 4259 sess2 4260 ordwe 4490 wessep 4492 peano2 4509 finds 4514 finds2 4515 relss 4626 ssrel 4627 ssrel2 4629 ssrelrel 4639 xpsspw 4651 relop 4689 cnvss 4712 dmss 4738 dmcosseq 4810 funss 5142 imadif 5203 imain 5205 fss 5284 fun 5295 brprcneu 5414 isores3 5716 isopolem 5723 isosolem 5725 tposfn2 6163 tposfo2 6164 tposf1o2 6167 smores 6189 tfr1onlemaccex 6245 tfrcllemaccex 6258 iinerm 6501 xpdom2 6725 ssenen 6745 exmidpw 6802 recexprlemlol 7434 recexprlemupu 7436 axpre-ltwlin 7691 axpre-apti 7693 nnindnn 7701 nnind 8736 uzind 9162 hashfacen 10579 cau3lem 10886 tgcl 12233 epttop 12259 txcnp 12440 |
Copyright terms: Public domain | W3C validator |