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 sbi1OLD 2542 sbi1ALT 2606 mopick 2710 isofrlem 7093 kmlem9 9584 squeeze0 11543 lcmfunsnlem1 15981 fgss2 22482 ordcmp 33795 linepsubN 36903 pmapsub 36919 ichreuopeq 43655 bgoldbnnsum3prm 43989 |
Copyright terms: Public domain | W3C validator |