Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3mix3d | Structured version Visualization version Unicode version |
Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
Ref | Expression |
---|---|
3mixd.1 |
Ref | Expression |
---|---|
3mix3d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3mixd.1 | . 2 | |
2 | 3mix3 1232 | . 2 | |
3 | 1, 2 | syl 17 | 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: funtpgOLD 5943 elfiun 8336 nnnegz 11380 hashv01gt1 13133 lcmfunsnlem2lem2 15352 cshwshashlem1 15802 dyaddisjlem 23363 zabsle1 25021 btwncolg3 25452 btwnlng3 25516 frgr3vlem2 27138 3vfriswmgr 27142 frgrregorufr0 27188 noextendgt 31823 sltsolem1 31826 nodense 31842 fnwe2lem3 37622 |
Copyright terms: Public domain | W3C validator |