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 294. 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 | syl5bir 246 | . 2 ⊢ (𝜑 → (𝜃 → 𝜒)) |
4 | 3imtr3g.3 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
5 | 3, 4 | syl6ib 254 | 1 ⊢ (𝜑 → (𝜃 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 |
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 210 |
This theorem is referenced by: aleximi 1839 sspwb 5331 ssopab2bw 5425 ssopab2b 5427 wetrep 5541 imadif 6461 ssoprab2b 7277 eqoprab2bw 7278 suceloni 7589 tfinds2 7639 iiner 8468 fsetcdmex 8541 fiint 8945 dfac5lem5 9738 axpowndlem3 10210 uzind 12266 isprm5 16261 funcres2 17401 fthres2 17436 ipodrsima 18044 subrgdvds 19811 hausflim 22875 dvres2 24806 axlowdimlem14 27043 atabs2i 30480 esum2dlem 31769 nn0prpw 34246 bj-hbext 34626 heibor1lem 35702 prter2 36630 dvelimf-o 36678 frege70 41216 frege72 41218 frege93 41239 frege110 41256 frege120 41266 pm11.71 41686 sbiota1 41723 |
Copyright terms: Public domain | W3C validator |