Theorem 3mix3 1129

Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Assertion

Ref	Expression
3mix3

Proof of Theorem 3mix3

Step	Hyp	Ref	Expression
1		3mix1 1127	. 2
2		3orrot 943	. 2
3	1, 2	sylib 190	1

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