![]() |
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 1139 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜒 |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: hartogslem2 9538 harwdom 9586 divalglem6 16341 structfn 17089 strleun 17090 oppchomfval 17658 sratset 20803 srads 20806 tngip 24162 dfrelog 26074 log2ub 26454 birthdaylem3 26458 birthday 26459 divsqrtsum2 26487 harmonicbnd2 26509 lgslem4 26803 lgscllem 26807 lgsdir2lem2 26829 lgsdir2lem3 26830 mulog2sumlem1 27037 siilem2 30105 h2hva 30227 h2hsm 30228 h2hnm 30229 elunop2 31266 wallispilem3 44783 wallispilem4 44784 prstchomval 47694 |
Copyright terms: Public domain | W3C validator |