![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4g | GIF version |
Description: More general version of 3imtr4i 199. 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 150 | . 2 ⊢ (𝜑 → (𝜃 → 𝜒)) |
4 | 3imtr4g.3 | . 2 ⊢ (𝜏 ↔ 𝜒) | |
5 | 3, 4 | syl6ibr 160 | 1 ⊢ (𝜑 → (𝜃 → 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 3anim123d 1251 3orim123d 1252 hbbid 1508 spsbim 1766 moim 2007 moimv 2009 2euswapdc 2034 ralim 2427 ralimdaa 2433 ralimdv2 2436 rexim 2460 reximdv2 2465 rmoim 2800 ssel 3002 sstr2 3015 sscon 3116 ssdif 3117 unss1 3151 ssrin 3207 prel12 3583 uniss 3642 ssuni 3643 intss 3677 intssunim 3678 iunss1 3709 iinss1 3710 ss2iun 3713 disjss2 3789 disjss1 3792 ssbrd 3846 sspwb 3999 poss 4081 pofun 4095 soss 4097 sess1 4120 sess2 4121 ordwe 4346 wessep 4348 peano2 4364 finds 4369 finds2 4370 relss 4473 ssrel 4474 ssrel2 4476 ssrelrel 4486 xpsspw 4498 relop 4534 cnvss 4556 dmss 4582 dmcosseq 4651 funss 4970 imadif 5030 imain 5032 fss 5105 fun 5114 brprcneu 5223 isores3 5507 isopolem 5513 isosolem 5515 tposfn2 5936 tposfo2 5937 tposf1o2 5940 smores 5962 tfr1onlemaccex 6018 tfrcllemaccex 6031 iinerm 6266 xpdom2 6397 recexprlemlol 6948 recexprlemupu 6950 axpre-ltwlin 7181 axpre-apti 7183 nnindnn 7191 nnind 8192 uzind 8609 cau3lem 10219 |
Copyright terms: Public domain | W3C validator |