Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp1i | 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 |
---|---|
simp1i | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1i.1 | . 2 ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) | |
2 | simp1 1054 | . 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: find 6983 hartogslem2 8331 harwdom 8378 divalglem6 14959 structfn 15708 strleun 15799 birthday 24481 divsqrsumf 24507 emcl 24529 lgslem4 24825 lgscllem 24829 lgsdir2lem2 24851 mulog2sumlem1 25023 siilem2 27091 h2hva 27215 h2hsm 27216 elunop2 28256 wallispilem3 38960 wallispilem4 38961 |
Copyright terms: Public domain | W3C validator |