![]() |
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 1135 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜒 |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: hartogslem2 9572 harwdom 9620 divalglem6 16380 structfn 17130 strleun 17131 oppchomfval 17699 sratset 21079 srads 21082 tngip 24580 dfrelog 26517 log2ub 26899 birthdaylem3 26903 birthday 26904 divsqrtsum2 26933 harmonicbnd2 26955 lgslem4 27251 lgscllem 27255 lgsdir2lem2 27277 lgsdir2lem3 27278 mulog2sumlem1 27485 siilem2 30680 h2hva 30802 h2hsm 30803 h2hnm 30804 elunop2 31841 wallispilem3 45457 wallispilem4 45458 prstchomval 48131 |
Copyright terms: Public domain | W3C validator |