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

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

Proof of Theorem 3mix3
StepHypRef Expression
1 3mix1 1165 . 2
2 3orrot 979 . 2
31, 2sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/w3o 972
This theorem is referenced by:  3mix3i  1170  3mix3d  1173  3jaob  1290  tpid3g  4145  tppreqb  4171  onzsl  6681  sornom  8678  fpwwe2lem13  9041  nn01to3  11204  qbtwnxr  11428  hash1to3  12530  cshwshashlem1  14580  ostth  23824  sltsolem1  29428  btwncolinear1  29719  limcicciooub  31643  tpres  32554  nn0le2is012  32956  tpid3gVD  33642
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