![]() |
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 1134 | . 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: hartogslem2 9568 harwdom 9616 divalglem6 16378 strleun 17129 oppcbas 17702 sratset 21086 srads 21089 tngvsca 24604 birthdaylem3 26930 birthday 26931 divsqrsum 26959 harmonicbnd 26981 lgslem4 27278 lgscllem 27282 lgsdir2lem2 27304 mulog2sum 27515 vmalogdivsum2 27516 siilem2 30734 h2hva 30856 h2hsm 30857 hhssabloi 31144 elunop2 31895 1fldgenq 33108 zlmds 33694 zlmtset 33696 wallispilem3 45593 wallispilem4 45594 prstcbas 48259 |
Copyright terms: Public domain | W3C validator |