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 2061 moimv 2063 2euswapdc 2088 nelcon3d 2412 ralim 2489 ralimdaa 2496 ralimdv2 2500 rexim 2524 reximdv2 2529 rmoim 2880 ssel 3086 sstr2 3099 ssrexf 3154 ssrmof 3155 sscon 3205 ssdif 3206 unss1 3240 ssrin 3296 prel12 3693 uniss 3752 ssuni 3753 intss 3787 intssunim 3788 iunss1 3819 iinss1 3820 ss2iun 3823 disjss2 3904 disjss1 3907 ssbrd 3966 sspwb 4133 poss 4215 pofun 4229 soss 4231 sess1 4254 sess2 4255 ordwe 4485 wessep 4487 peano2 4504 finds 4509 finds2 4510 relss 4621 ssrel 4622 ssrel2 4624 ssrelrel 4634 xpsspw 4646 relop 4684 cnvss 4707 dmss 4733 dmcosseq 4805 funss 5137 imadif 5198 imain 5200 fss 5279 fun 5290 brprcneu 5407 isores3 5709 isopolem 5716 isosolem 5718 tposfn2 6156 tposfo2 6157 tposf1o2 6160 smores 6182 tfr1onlemaccex 6238 tfrcllemaccex 6251 iinerm 6494 xpdom2 6718 ssenen 6738 exmidpw 6795 recexprlemlol 7427 recexprlemupu 7429 axpre-ltwlin 7684 axpre-apti 7686 nnindnn 7694 nnind 8729 uzind 9155 hashfacen 10572 cau3lem 10879 tgcl 12222 epttop 12248 txcnp 12429 |
Copyright terms: Public domain | W3C validator |