![]() |
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 1083 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜒 |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1054 |
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 197 df-an 385 df-3an 1056 |
This theorem is referenced by: hartogslem2 8489 harwdom 8536 divalglem6 15168 structfn 15921 strleun 16019 dfrelog 24357 log2ub 24721 birthdaylem3 24725 birthday 24726 divsqrtsum2 24754 harmonicbnd2 24776 lgslem4 25070 lgscllem 25074 lgsdir2lem2 25096 lgsdir2lem3 25097 mulog2sumlem1 25268 siilem2 27835 h2hva 27959 h2hsm 27960 h2hnm 27961 elunop2 29000 wallispilem3 40602 wallispilem4 40603 |
Copyright terms: Public domain | W3C validator |