![]() |
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 1133 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: find 7908 findOLD 7909 hartogslem2 9574 harwdom 9622 divalglem6 16382 structfn 17132 strleun 17133 oppcbas 17706 rescbas 17819 rescabs 17825 rmodislmod 20820 rmodislmodOLD 20821 sratset 21081 srads 21084 tngsca 24578 birthday 26906 divsqrsumf 26933 emcl 26955 lgslem4 27253 lgscllem 27257 lgsdir2lem2 27279 mulog2sumlem1 27487 siilem2 30682 h2hva 30804 h2hsm 30805 elunop2 31843 zlmds 33596 zlmtset 33598 wallispilem3 45484 wallispilem4 45485 prstcbas 48151 |
Copyright terms: Public domain | W3C validator |