Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3anim3i | Structured version Visualization version Unicode version |
Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.) |
Ref | Expression |
---|---|
3animi.1 |
Ref | Expression |
---|---|
3anim3i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 | |
2 | id 22 | . 2 | |
3 | 3animi.1 | . 2 | |
4 | 1, 2, 3 | 3anim123i 1247 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 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: syl3anl3 1376 syl3anr3 1380 elioo4g 12234 ssnn0fi 12784 tmdcn2 21893 axcont 25856 1ewlk 26976 1pthon2ve 27014 numclwwlk3OLD 27242 numclwwlk3 27243 minvecolem3 27732 bnj556 30970 bnj557 30971 bnj1145 31061 btwnconn1lem4 32197 btwnconn1lem5 32198 btwnconn1lem6 32199 bj-ceqsalt 32875 bj-ceqsaltv 32876 |
Copyright terms: Public domain | W3C validator |