![]() |
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 290. 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 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 1834 rexim 3086 sspwb 5442 ssopab2bw 5540 ssopab2b 5542 wetrep 5662 imadif 6621 ssoprab2b 7462 eqoprab2bw 7463 sucexeloniOLD 7781 suceloniOLD 7783 tfinds2 7836 iiner 8766 fsetcdmex 8840 fiint 9307 dfac5lem5 10104 axpowndlem3 10576 uzind 12636 isprm5 16626 funcres2 17830 fthres2 17865 ipodrsima 18476 subrgdvds 20326 hausflim 23414 dvres2 25358 axlowdimlem14 28078 atabs2i 31518 esum2dlem 32921 nn0prpw 35012 bj-hbext 35392 heibor1lem 36482 prter2 37556 dvelimf-o 37604 frege70 42455 frege72 42457 frege93 42478 frege110 42495 frege120 42505 pm11.71 42927 sbiota1 42964 |
Copyright terms: Public domain | W3C validator |