![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl5d | Structured version Visualization version GIF version |
Description: A nested syllogism deduction. Deduction associated with syl5 34. (Contributed by NM, 14-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.) |
Ref | Expression |
---|---|
syl5d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
syl5d.2 | ⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏))) |
Ref | Expression |
---|---|
syl5d | ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5d.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | a1d 25 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒))) |
3 | syl5d.2 | . 2 ⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏))) | |
4 | 2, 3 | syldd 72 | 1 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: syl7 74 syl9 77 imim12d 81 mopick 2623 isofrlem 7360 kmlem9 10197 squeeze0 12169 lcmfunsnlem1 16671 rnglidlmcl 21244 fgss2 23898 ordcmp 36430 linepsubN 39735 pmapsub 39751 ichreuopeq 47398 bgoldbnnsum3prm 47729 grimedg 47841 |
Copyright terms: Public domain | W3C validator |