![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syld3an1 | Structured version Visualization version GIF version |
Description: A syllogism inference. (Contributed by NM, 7-Jul-2008.) (Proof shortened by Wolf Lammen, 26-Jun-2022.) |
Ref | Expression |
---|---|
syld3an1.1 | ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑) |
syld3an1.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syld3an1 | ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syld3an1.1 | . 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑) | |
2 | simp2 1137 | . 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓) | |
3 | simp3 1138 | . 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃) | |
4 | syld3an1.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1371 | 1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 |
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 df-an 397 df-3an 1089 |
This theorem is referenced by: f1dom2g 8905 f1domfi2 9125 entrfi 9133 entrfir 9134 domtrfil 9135 domtrfi 9136 domtrfir 9137 php3 9152 findcard3 9225 npncan 11418 nnpcan 11420 ppncan 11439 muldivdir 11844 subdivcomb1 11846 div2neg 11874 ltmuldiv 12024 opfi1uzind 14392 sgrp2nmndlem4 18730 zndvds 20941 wsuceq123 34259 atlrelat1 37750 cvlatcvr1 37770 dih11 39695 wessf1ornlem 43339 mullimc 43789 mullimcf 43796 icccncfext 44060 stoweidlem34 44207 stoweidlem49 44222 stoweidlem57 44230 sigarexp 45032 f1ocof1ob 45245 el0ldepsnzr 46480 |
Copyright terms: Public domain | W3C validator |