![]() |
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 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: hartogslem2 9537 harwdom 9585 divalglem6 16340 structfn 17088 strleun 17089 oppchomfval 17657 sratset 20802 srads 20805 tngip 24161 dfrelog 26073 log2ub 26451 birthdaylem3 26455 birthday 26456 divsqrtsum2 26484 harmonicbnd2 26506 lgslem4 26800 lgscllem 26804 lgsdir2lem2 26826 lgsdir2lem3 26827 mulog2sumlem1 27034 siilem2 30100 h2hva 30222 h2hsm 30223 h2hnm 30224 elunop2 31261 wallispilem3 44773 wallispilem4 44774 prstchomval 47684 |
Copyright terms: Public domain | W3C validator |