![]() |
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 8916 f1domfi2 9136 entrfi 9144 entrfir 9145 domtrfil 9146 domtrfi 9147 domtrfir 9148 php3 9163 findcard3 9236 npncan 11431 nnpcan 11433 ppncan 11452 muldivdir 11857 subdivcomb1 11859 div2neg 11887 ltmuldiv 12037 opfi1uzind 14412 sgrp2nmndlem4 18752 zndvds 20993 wsuceq123 34475 atlrelat1 37856 cvlatcvr1 37876 dih11 39801 wessf1ornlem 43525 mullimc 43977 mullimcf 43984 icccncfext 44248 stoweidlem34 44395 stoweidlem49 44410 stoweidlem57 44418 sigarexp 45220 f1ocof1ob 45433 el0ldepsnzr 46668 |
Copyright terms: Public domain | W3C validator |