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 1128 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: find 7596 hartogslem2 8995 harwdom 9042 divalglem6 15737 structfn 16488 strleun 16579 rmodislmod 19631 birthday 25459 divsqrsumf 25485 emcl 25507 lgslem4 25803 lgscllem 25807 lgsdir2lem2 25829 mulog2sumlem1 26037 siilem2 28556 h2hva 28678 h2hsm 28679 elunop2 29717 wallispilem3 42229 wallispilem4 42230 |
Copyright terms: Public domain | W3C validator |