![]() |
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 1137 | . 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: find 7887 findOLD 7888 hartogslem2 9538 harwdom 9586 divalglem6 16341 structfn 17089 strleun 17090 oppcbas 17663 rescbas 17776 rescabs 17782 rmodislmod 20540 rmodislmodOLD 20541 sratset 20803 srads 20806 tngsca 24158 birthday 26459 divsqrsumf 26485 emcl 26507 lgslem4 26803 lgscllem 26807 lgsdir2lem2 26829 mulog2sumlem1 27037 siilem2 30105 h2hva 30227 h2hsm 30228 elunop2 31266 zlmds 32942 zlmtset 32944 wallispilem3 44783 wallispilem4 44784 prstcbas 47687 |
Copyright terms: Public domain | W3C validator |