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 1139 | . 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓) | |
3 | simp3 1140 | . 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃) | |
4 | syld3an1.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1373 | 1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: entrfi 8843 entrfir 8844 npncan 11064 nnpcan 11066 ppncan 11085 muldivdir 11490 subdivcomb1 11492 div2neg 11520 ltmuldiv 11670 opfi1uzind 14032 sgrp2nmndlem4 18309 zndvds 20468 wsuceq123 33488 atlrelat1 37021 cvlatcvr1 37041 dih11 38965 wessf1ornlem 42336 mullimc 42775 mullimcf 42782 icccncfext 43046 stoweidlem34 43193 stoweidlem49 43208 stoweidlem57 43216 sigarexp 43990 f1ocof1ob 44188 el0ldepsnzr 45424 |
Copyright terms: Public domain | W3C validator |