![]() |
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 1010 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
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 189 df-an 373 df-3an 988 |
This theorem is referenced by: hartogslem2 8063 harwdom 8110 divalglem6 14390 strleun 15232 birthdaylem3 23891 birthday 23892 divsqrsum 23919 harmonicbnd 23941 lgslem4 24239 lgscllem 24243 lgsdir2lem2 24264 mulog2sum 24387 vmalogdivsum2 24388 siilem2 26505 h2hva 26639 h2hsm 26640 hhssabloi 26925 elunop2 27678 wallispilem3 37939 wallispilem4 37940 |
Copyright terms: Public domain | W3C validator |