| 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 1137 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: find 7917 hartogslem2 9583 harwdom 9631 divalglem6 16435 structfn 17193 strleun 17194 oppcbas 17761 rescbas 17873 rescabs 17877 rmodislmod 20928 sratset 21188 srads 21191 tngsca 24662 birthday 26997 divsqrsumf 27024 emcl 27046 lgslem4 27344 lgscllem 27348 lgsdir2lem2 27370 mulog2sumlem1 27578 siilem2 30871 h2hva 30993 h2hsm 30994 elunop2 32032 zlmds 33961 zlmtset 33963 wallispilem3 46082 wallispilem4 46083 prstcbas 49156 |
| Copyright terms: Public domain | W3C validator |