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

Theorem 3mix3 1126
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 1124 . 2  |-  ( ph  ->  ( ph  \/  ps  \/  ch ) )
2 3orrot 940 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )
31, 2sylib 188 1  |-  ( ph  ->  ( ps  \/  ch  \/  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 933
This theorem is referenced by:  3mix3i  1129  3jaob  1244  tpid3g  3754  onzsl  4653  elfiun  7199  sornom  7919  fpwwe2lem13  8280  qbtwnxr  10543  dyaddisjlem  18966  ostth  20804  3mix3d  24084  sltsolem1  24393  btwncolinear1  24764  sgplpte21d2  26243  xsyysx  26248  fnwe2lem3  27252  spthispth  28359  frgra3vlem2  28425  3vfriswmgra  28429  tpid3gVD  28934
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 177  df-or 359  df-3or 935
  Copyright terms: Public domain W3C validator