![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp1i | 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 |
---|---|
simp1i | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1i.1 | . 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) | |
2 | simp1 1170 | . 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: find 7357 hartogslem2 8724 harwdom 8771 divalglem6 15502 structfn 16246 strleun 16338 rmodislmod 19294 birthday 25101 divsqrsumf 25127 emcl 25149 lgslem4 25445 lgscllem 25449 lgsdir2lem2 25471 mulog2sumlem1 25643 siilem2 28258 h2hva 28382 h2hsm 28383 elunop2 29423 wallispilem3 41072 wallispilem4 41073 |
Copyright terms: Public domain | W3C validator |