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

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

Proof of Theorem 3mix3
StepHypRef Expression
1 3mix1 1127 . 2
2 3orrot 943 . 2
31, 2sylib 190 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  \/w3o 936
This theorem is referenced by:  3mix3i  1132  3jaob  1247  tpid3g  3951  tppreqb  3971  onzsl  4871  funtpg  5552  elfiun  7488  sornom  8212  fpwwe2lem13  8572  qbtwnxr  10841  hashv01gt1  11684  dyaddisjlem  19523  ostth  21369  spthispth  21609  3mix3d  25432  sltsolem1  25883  btwncolinear1  26263  fnwe2lem3  27462  cshwoor  28591  frgra3vlem2  28785  3vfriswmgra  28789  frgraregorufr0  28835  2spotdisj  28844  tpid3gVD  29351
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 179  df-or 361  df-3or 938
  Copyright terms: Public domain W3C validator