![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp3i | Structured version Visualization version GIF version |
Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
Ref | Expression |
---|---|
3simp1i.1 | ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) |
Ref | Expression |
---|---|
simp3i | ⊢ 𝜒 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1i.1 | . 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) | |
2 | simp3 1172 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜒 |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1111 |
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 199 df-an 387 df-3an 1113 |
This theorem is referenced by: hartogslem2 8724 harwdom 8771 divalglem6 15502 structfn 16246 strleun 16338 dfrelog 24718 log2ub 25096 birthdaylem3 25100 birthday 25101 divsqrtsum2 25129 harmonicbnd2 25151 lgslem4 25445 lgscllem 25449 lgsdir2lem2 25471 lgsdir2lem3 25472 mulog2sumlem1 25643 siilem2 28258 h2hva 28382 h2hsm 28383 h2hnm 28384 elunop2 29423 wallispilem3 41072 wallispilem4 41073 |
Copyright terms: Public domain | W3C validator |