Theorem 3mix3 1167

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 1165	. 2
2		3orrot 979	. 2
3	1, 2	sylib 196	1

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