![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4g | GIF version |
Description: More general version of 3imtr4i 190. 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 141 | . 2 ⊢ (φ → (θ → χ)) |
4 | 3imtr4g.3 | . 2 ⊢ (τ ↔ χ) | |
5 | 3, 4 | syl6ibr 151 | 1 ⊢ (φ → (θ → τ)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3anim123d 1213 3orim123d 1214 hbbid 1464 spsbim 1721 moim 1961 moimv 1963 2euswapdc 1988 ralim 2374 ralimdaa 2380 ralimdv2 2383 rexim 2407 reximdv2 2412 rmoim 2734 ssel 2933 sstr2 2946 sscon 3071 ssdif 3072 unss1 3106 ssrin 3156 prel12 3533 uniss 3592 ssuni 3593 intss 3627 intssunim 3628 iunss1 3659 iinss1 3660 ss2iun 3663 disjss2 3739 disjss1 3742 ssbrd 3796 sspwb 3943 poss 4026 pofun 4040 soss 4042 sess1 4059 sess2 4060 peano2 4261 finds 4266 finds2 4267 relss 4370 ssrel 4371 ssrel2 4373 ssrelrel 4383 xpsspw 4393 relop 4429 cnvss 4451 dmss 4477 dmcosseq 4546 funss 4863 imadif 4922 imain 4924 fss 4997 fun 5006 brprcneu 5114 isores3 5398 isopolem 5404 isosolem 5406 tposfn2 5822 tposfo2 5823 tposf1o2 5826 smores 5848 iinerm 6114 xpdom2 6241 recexprlemlol 6598 recexprlemupu 6600 axpre-ltwlin 6767 axpre-apti 6769 nnind 7711 uzind 8125 |
Copyright terms: Public domain | W3C validator |