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

Theorem 3mix3 1128
Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
Assertion
Ref Expression
3mix3  |-  ( ph  ->  ( ps  \/  ch  \/  ph ) )

Proof of Theorem 3mix3
StepHypRef Expression
1 3mix1 1126 . 2  |-  ( ph  ->  ( ph  \/  ps  \/  ch ) )
2 3orrot 942 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )
31, 2sylib 189 1  |-  ( ph  ->  ( ps  \/  ch  \/  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 935
This theorem is referenced by:  3mix3i  1131  3jaob  1246  tpid3g  3855  tppreqb  3875  onzsl  4759  funtpg  5434  elfiun  7363  sornom  8083  fpwwe2lem13  8443  qbtwnxr  10711  hashv01gt1  11549  dyaddisjlem  19347  ostth  21193  spthispth  21420  3mix3d  24944  sltsolem1  25339  btwncolinear1  25710  fnwe2lem3  26811  frgra3vlem2  27747  3vfriswmgra  27751  frgraregorufr0  27797  tpid3gVD  28288
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360  df-3or 937
  Copyright terms: Public domain W3C validator