MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3mix2 Unicode version

Theorem 3mix2 1166
Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
Assertion
Ref Expression
3mix2

Proof of Theorem 3mix2
StepHypRef Expression
1 3mix1 1165 . 2
2 3orrot 979 . 2
31, 2sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/w3o 972
This theorem is referenced by:  3mix2i  1169  3mix2d  1172  3jaob  1290  tppreqb  4171  onzsl  6681  sornom  8678  hash1to3  12530  cshwshashlem1  14580  ostth  23824  sltsolem1  29428  nodenselem8  29448  fnwe2lem3  30998  tpres  32554  nn0le2is012  32956
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 185  df-or 370  df-3or 974
  Copyright terms: Public domain W3C validator