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 1138 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: find 7683 findOLD 7684 hartogslem2 9172 harwdom 9220 divalglem6 15972 structfn 16722 strleun 16723 rmodislmod 19980 birthday 25850 divsqrsumf 25876 emcl 25898 lgslem4 26194 lgscllem 26198 lgsdir2lem2 26220 mulog2sumlem1 26428 siilem2 28946 h2hva 29068 h2hsm 29069 elunop2 30107 wallispilem3 43298 wallispilem4 43299 prstcbas 46036 |
Copyright terms: Public domain | W3C validator |