![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3imtr3g | Structured version Visualization version GIF version |
Description: More general version of 3imtr3i 291. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
Ref | Expression |
---|---|
3imtr3g.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
3imtr3g.2 | ⊢ (𝜓 ↔ 𝜃) |
3imtr3g.3 | ⊢ (𝜒 ↔ 𝜏) |
Ref | Expression |
---|---|
3imtr3g | ⊢ (𝜑 → (𝜃 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imtr3g.2 | . . 3 ⊢ (𝜓 ↔ 𝜃) | |
2 | 3imtr3g.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | biimtrrid 242 | . 2 ⊢ (𝜑 → (𝜃 → 𝜒)) |
4 | 3imtr3g.3 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
5 | 3, 4 | syl6ib 251 | 1 ⊢ (𝜑 → (𝜃 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 |
This theorem is referenced by: aleximi 1835 rexim 3087 sspwb 5410 ssopab2bw 5508 ssopab2b 5510 wetrep 5630 imadif 6589 ssoprab2b 7430 eqoprab2bw 7431 sucexeloniOLD 7749 suceloniOLD 7751 tfinds2 7804 iiner 8734 fsetcdmex 8807 fiint 9274 dfac5lem5 10071 axpowndlem3 10543 uzind 12603 isprm5 16591 funcres2 17792 fthres2 17827 ipodrsima 18438 subrgdvds 20278 hausflim 23355 dvres2 25299 axlowdimlem14 27953 atabs2i 31393 esum2dlem 32755 nn0prpw 34848 bj-hbext 35228 heibor1lem 36318 prter2 37393 dvelimf-o 37441 frege70 42297 frege72 42299 frege93 42320 frege110 42337 frege120 42347 pm11.71 42769 sbiota1 42806 |
Copyright terms: Public domain | W3C validator |