Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp2i | 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 |
---|---|
simp2i | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1i.1 | . 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) | |
2 | simp2 1055 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: hartogslem2 8331 harwdom 8378 divalglem6 14959 strleun 15799 birthdaylem3 24480 birthday 24481 divsqrsum 24508 harmonicbnd 24530 lgslem4 24825 lgscllem 24829 lgsdir2lem2 24851 mulog2sum 25026 vmalogdivsum2 25027 siilem2 27091 h2hva 27215 h2hsm 27216 hhssabloi 27503 elunop2 28256 wallispilem3 38960 wallispilem4 38961 |
Copyright terms: Public domain | W3C validator |