| 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 1138 | . 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓) | |
| 3 | simp3 1139 | . 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃) | |
| 4 | syld3an1.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
| 5 | 1, 2, 3, 4 | syl3anc 1373 | 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: f1dom2g 9010 f1domfi2 9222 entrfi 9230 entrfir 9231 domtrfil 9232 domtrfi 9233 domtrfir 9234 php3 9249 findcard3 9318 npncan 11530 nnpcan 11532 ppncan 11551 muldivdir 11960 subdivcomb1 11962 div2neg 11990 ltmuldiv 12141 opfi1uzind 14550 sgrp2nmndlem4 18941 zndvds 21568 wsuceq123 35815 atlrelat1 39322 cvlatcvr1 39342 dih11 41267 wessf1ornlem 45190 mullimc 45631 mullimcf 45638 icccncfext 45902 stoweidlem34 46049 stoweidlem49 46064 stoweidlem57 46072 sigarexp 46874 f1ocof1ob 47093 el0ldepsnzr 48384 |
| Copyright terms: Public domain | W3C validator |