Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3mix1d | Structured version Visualization version Unicode version |
Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
Ref | Expression |
---|---|
3mixd.1 |
Ref | Expression |
---|---|
3mix1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3mixd.1 | . 2 | |
2 | 3mix1 1230 | . 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: f1dom3fv3dif 6525 f1dom3el3dif 6526 elfiun 8336 prinfzo0 12506 lcmfunsnlem2lem2 15352 estrreslem2 16778 ostth 25328 btwncolg1 25450 hlln 25502 btwnlng1 25514 noextendlt 31822 sltsolem1 31826 nodense 31842 colineartriv1 32174 fnwe2lem3 37622 dfxlim2v 40073 |
Copyright terms: Public domain | W3C validator |