| 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 1138 | . 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 strleun 17194 oppcbas 17761 sratset 21188 srads 21191 tngvsca 24664 birthdaylem3 26996 birthday 26997 divsqrsum 27025 harmonicbnd 27047 lgslem4 27344 lgscllem 27348 lgsdir2lem2 27370 mulog2sum 27581 vmalogdivsum2 27582 siilem2 30871 h2hva 30993 h2hsm 30994 hhssabloi 31281 elunop2 32032 1fldgenq 33324 zlmds 33961 zlmtset 33963 wallispilem3 46082 wallispilem4 46083 prstcbas 49156 |
| Copyright terms: Public domain | W3C validator |