Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3mix2 | Structured version Visualization version Unicode version |
Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Ref | Expression |
---|---|
3mix2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3mix1 1230 | . 2 | |
2 | 3orrot 1044 | . 2 | |
3 | 1, 2 | sylibr 224 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 w3o 1036 |
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-or 385 df-3or 1038 |
This theorem is referenced by: 3mix2i 1234 3mix2d 1237 3jaob 1390 tppreqb 4336 tpres 6466 onzsl 7046 sornom 9099 nn0le2is012 11441 hash1to3 13273 cshwshashlem1 15802 zabsle1 25021 ostth 25328 nolesgn2o 31824 sltsolem1 31826 nosep1o 31832 nodenselem8 31841 fnwe2lem3 37622 dfxlim2v 40073 |
Copyright terms: Public domain | W3C validator |