![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4g | Unicode version |
Description: More general version of 3imtr4i 201. 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 | biimtrid 152 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3imtr4g.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | imbitrrdi 162 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3anim123d 1319 3orim123d 1320 hbbid 1575 spsbim 1843 moim 2090 moimv 2092 2euswapdc 2117 nelcon3d 2453 ralim 2536 ralimdaa 2543 ralimdv2 2547 rexim 2571 reximdv2 2576 rmoim 2940 ssel 3151 sstr2 3164 ssrexf 3219 ssrmof 3220 sscon 3271 ssdif 3272 unss1 3306 ssrin 3362 prel12 3773 uniss 3832 ssuni 3833 intss 3867 intssunim 3868 iunss1 3899 iinss1 3900 ss2iun 3903 disjss2 3985 disjss1 3988 ssbrd 4048 sspwb 4218 poss 4300 pofun 4314 soss 4316 sess1 4339 sess2 4340 ordwe 4577 wessep 4579 peano2 4596 finds 4601 finds2 4602 relss 4715 ssrel 4716 ssrel2 4718 ssrelrel 4728 xpsspw 4740 relop 4779 cnvss 4802 dmss 4828 dmcosseq 4900 funss 5237 imadif 5298 imain 5300 fss 5379 fun 5390 brprcneu 5510 isores3 5819 isopolem 5826 isosolem 5828 tposfn2 6270 tposfo2 6271 tposf1o2 6274 smores 6296 tfr1onlemaccex 6352 tfrcllemaccex 6365 iinerm 6610 xpdom2 6834 ssenen 6854 exmidpw 6911 exmidpweq 6912 nnnninfeq2 7130 recexprlemlol 7628 recexprlemupu 7630 axpre-ltwlin 7885 axpre-apti 7887 nnindnn 7895 nnind 8938 uzind 9367 hashfacen 10819 cau3lem 11126 tgcl 13704 epttop 13730 txcnp 13911 |
Copyright terms: Public domain | W3C validator |