Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp2i | Structured version Visualization version Unicode 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 1062 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: hartogslem2 8448 harwdom 8495 divalglem6 15121 strleun 15972 birthdaylem3 24680 birthday 24681 divsqrsum 24708 harmonicbnd 24730 lgslem4 25025 lgscllem 25029 lgsdir2lem2 25051 mulog2sum 25226 vmalogdivsum2 25227 siilem2 27707 h2hva 27831 h2hsm 27832 hhssabloi 28119 elunop2 28872 wallispilem3 40284 wallispilem4 40285 |
Copyright terms: Public domain | W3C validator |