| 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 243 | . 2 ⊢ (𝜑 → (𝜃 → 𝜒)) |
| 4 | 3imtr3g.3 | . 2 ⊢ (𝜒 ↔ 𝜏) | |
| 5 | 3, 4 | imbitrdi 251 | 1 ⊢ (𝜑 → (𝜃 → 𝜏)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: aleximi 1832 rexim 3087 sspwb 5454 ssopab2bw 5552 ssopab2b 5554 wetrep 5678 imadif 6650 ssoprab2b 7502 eqoprab2bw 7503 sucexeloniOLD 7830 suceloniOLD 7832 tfinds2 7885 iiner 8829 fsetcdmex 8903 fiint 9366 fiintOLD 9367 dfac5lem5 10167 axpowndlem3 10639 uzind 12710 isprm5 16744 funcres2 17943 fthres2 17979 ipodrsima 18586 subrgdvds 20586 hausflim 23989 dvres2 25947 precsexlem11 28241 uzsind 28391 axlowdimlem14 28970 atabs2i 32421 esum2dlem 34093 nn0prpw 36324 bj-hbext 36711 heibor1lem 37816 prter2 38882 dvelimf-o 38930 frege70 43946 frege72 43948 frege93 43969 frege110 43986 frege120 43996 pm11.71 44416 sbiota1 44453 |
| Copyright terms: Public domain | W3C validator |