|   | 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 2624 isofrlem 7361 kmlem9 10200 squeeze0 12172 lcmfunsnlem1 16675 rnglidlmcl 21227 fgss2 23883 ordcmp 36449 linepsubN 39755 pmapsub 39771 relpfrlem 44979 ichreuopeq 47465 bgoldbnnsum3prm 47796 grimedg 47908 | 
| Copyright terms: Public domain | W3C validator |