Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp1i | 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 |
---|---|
simp1i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1i.1 | . 2 | |
2 | simp1 1061 | . 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: find 7091 hartogslem2 8448 harwdom 8495 divalglem6 15121 structfn 15874 strleun 15972 rmodislmod 18931 birthday 24681 divsqrsumf 24707 emcl 24729 lgslem4 25025 lgscllem 25029 lgsdir2lem2 25051 mulog2sumlem1 25223 siilem2 27707 h2hva 27831 h2hsm 27832 elunop2 28872 wallispilem3 40284 wallispilem4 40285 |
Copyright terms: Public domain | W3C validator |