![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4g | GIF 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: → wi 4 ↔ wb 105 |
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 1330 3orim123d 1331 hbbid 1586 spsbim 1854 moim 2102 moimv 2104 2euswapdc 2129 nelcon3d 2466 ralim 2549 ralimdaa 2556 ralimdv2 2560 rexim 2584 reximdv2 2589 rmoim 2953 ssel 3164 sstr2 3177 ssrexf 3232 ssrmof 3233 sscon 3284 ssdif 3285 unss1 3319 ssrin 3375 prel12 3786 uniss 3845 ssuni 3846 intss 3880 intssunim 3881 iunss1 3912 iinss1 3913 ss2iun 3916 disjss2 3998 disjss1 4001 ssbrd 4061 sspwb 4234 poss 4316 pofun 4330 soss 4332 sess1 4355 sess2 4356 ordwe 4593 wessep 4595 peano2 4612 finds 4617 finds2 4618 relss 4731 ssrel 4732 ssrel2 4734 ssrelrel 4744 xpsspw 4756 relop 4795 cnvss 4818 dmss 4844 dmcosseq 4916 funss 5254 imadif 5315 imain 5317 fss 5396 fun 5407 brprcneu 5527 isores3 5837 isopolem 5844 isosolem 5846 tposfn2 6292 tposfo2 6293 tposf1o2 6296 smores 6318 tfr1onlemaccex 6374 tfrcllemaccex 6387 iinerm 6634 xpdom2 6858 ssenen 6880 exmidpw 6937 exmidpweq 6938 nnnninfeq2 7158 recexprlemlol 7656 recexprlemupu 7658 axpre-ltwlin 7913 axpre-apti 7915 nnindnn 7923 nnind 8966 uzind 9395 hashfacen 10851 cau3lem 11158 tgcl 14041 epttop 14067 txcnp 14248 |
Copyright terms: Public domain | W3C validator |