| 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 1139 | . 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: hartogslem2 9583 harwdom 9631 divalglem6 16435 structfn 17193 strleun 17194 oppchomfval 17757 sratset 21188 srads 21191 tngip 24666 dfrelog 26607 log2ub 26992 birthdaylem3 26996 birthday 26997 divsqrtsum2 27026 harmonicbnd2 27048 lgslem4 27344 lgscllem 27348 lgsdir2lem2 27370 lgsdir2lem3 27371 mulog2sumlem1 27578 siilem2 30871 h2hva 30993 h2hsm 30994 h2hnm 30995 elunop2 32032 wallispilem3 46082 wallispilem4 46083 prstchomval 49163 |
| Copyright terms: Public domain | W3C validator |