![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4g | GIF 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-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 1262 3orim123d 1263 hbbid 1519 spsbim 1778 moim 2019 moimv 2021 2euswapdc 2046 nelcon3d 2368 ralim 2445 ralimdaa 2452 ralimdv2 2455 rexim 2479 reximdv2 2484 rmoim 2830 ssel 3033 sstr2 3046 sscon 3149 ssdif 3150 unss1 3184 ssrin 3240 prel12 3637 uniss 3696 ssuni 3697 intss 3731 intssunim 3732 iunss1 3763 iinss1 3764 ss2iun 3767 disjss2 3847 disjss1 3850 ssbrd 3908 sspwb 4067 poss 4149 pofun 4163 soss 4165 sess1 4188 sess2 4189 ordwe 4419 wessep 4421 peano2 4438 finds 4443 finds2 4444 relss 4554 ssrel 4555 ssrel2 4557 ssrelrel 4567 xpsspw 4579 relop 4617 cnvss 4640 dmss 4666 dmcosseq 4736 funss 5068 imadif 5128 imain 5130 fss 5207 fun 5218 brprcneu 5333 isores3 5632 isopolem 5639 isosolem 5641 tposfn2 6069 tposfo2 6070 tposf1o2 6073 smores 6095 tfr1onlemaccex 6151 tfrcllemaccex 6164 iinerm 6404 xpdom2 6627 ssenen 6647 exmidpw 6704 recexprlemlol 7282 recexprlemupu 7284 axpre-ltwlin 7515 axpre-apti 7517 nnindnn 7525 nnind 8536 uzind 8956 hashfacen 10372 cau3lem 10678 tgcl 11932 epttop 11958 |
Copyright terms: Public domain | W3C validator |