![]() |
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: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3anim123d 1280 3orim123d 1281 hbbid 1537 spsbim 1797 moim 2039 moimv 2041 2euswapdc 2066 nelcon3d 2388 ralim 2465 ralimdaa 2472 ralimdv2 2476 rexim 2500 reximdv2 2505 rmoim 2854 ssel 3057 sstr2 3070 ssrexf 3125 ssrmof 3126 sscon 3176 ssdif 3177 unss1 3211 ssrin 3267 prel12 3664 uniss 3723 ssuni 3724 intss 3758 intssunim 3759 iunss1 3790 iinss1 3791 ss2iun 3794 disjss2 3875 disjss1 3878 ssbrd 3936 sspwb 4098 poss 4180 pofun 4194 soss 4196 sess1 4219 sess2 4220 ordwe 4450 wessep 4452 peano2 4469 finds 4474 finds2 4475 relss 4586 ssrel 4587 ssrel2 4589 ssrelrel 4599 xpsspw 4611 relop 4649 cnvss 4672 dmss 4698 dmcosseq 4768 funss 5100 imadif 5161 imain 5163 fss 5242 fun 5253 brprcneu 5368 isores3 5670 isopolem 5677 isosolem 5679 tposfn2 6117 tposfo2 6118 tposf1o2 6121 smores 6143 tfr1onlemaccex 6199 tfrcllemaccex 6212 iinerm 6455 xpdom2 6678 ssenen 6698 exmidpw 6755 recexprlemlol 7382 recexprlemupu 7384 axpre-ltwlin 7618 axpre-apti 7620 nnindnn 7628 nnind 8646 uzind 9066 hashfacen 10472 cau3lem 10778 tgcl 12076 epttop 12102 txcnp 12282 |
Copyright terms: Public domain | W3C validator |