![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp2i | 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 |
---|---|
simp2i | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1i.1 | . 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) | |
2 | simp2 1173 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1113 |
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 1115 |
This theorem is referenced by: hartogslem2 8717 harwdom 8764 divalglem6 15495 strleun 16331 birthdaylem3 25093 birthday 25094 divsqrsum 25121 harmonicbnd 25143 lgslem4 25438 lgscllem 25442 lgsdir2lem2 25464 mulog2sum 25639 vmalogdivsum2 25640 siilem2 28262 h2hva 28386 h2hsm 28387 hhssabloi 28674 elunop2 29427 wallispilem3 41078 wallispilem4 41079 |
Copyright terms: Public domain | W3C validator |