![]() |
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 | imbitrdi 250 | 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 3088 sspwb 5450 ssopab2bw 5548 ssopab2b 5550 wetrep 5670 imadif 6633 ssoprab2b 7478 eqoprab2bw 7479 sucexeloniOLD 7798 suceloniOLD 7800 tfinds2 7853 iiner 8783 fsetcdmex 8857 fiint 9324 dfac5lem5 10122 axpowndlem3 10594 uzind 12654 isprm5 16644 funcres2 17848 fthres2 17883 ipodrsima 18494 subrgdvds 20333 hausflim 23485 dvres2 25429 precsexlem11 27666 axlowdimlem14 28244 atabs2i 31686 esum2dlem 33121 nn0prpw 35256 bj-hbext 35636 heibor1lem 36725 prter2 37799 dvelimf-o 37847 frege70 42732 frege72 42734 frege93 42755 frege110 42772 frege120 42782 pm11.71 43204 sbiota1 43241 |
Copyright terms: Public domain | W3C validator |