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

Theorem 3mix3 1159
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 1157 . 2  |-  ( ph  ->  ( ph  \/  ps  \/  ch ) )
2 3orrot 971 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )
31, 2sylib 196 1  |-  ( ph  ->  ( ps  \/  ch  \/  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 964
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 966
This theorem is referenced by:  3mix3i  1162  3mix3d  1165  3jaob  1280  tpid3g  3990  tppreqb  4014  funtpg  5468  onzsl  6457  elfiun  7680  sornom  8446  fpwwe2lem13  8809  qbtwnxr  11170  hashv01gt1  12116  cshwshashlem1  14122  dyaddisjlem  21075  ostth  22888  spthispth  23472  sltsolem1  27809  btwncolinear1  28100  fnwe2lem3  29405  nn01to3  30187  hash1to3  30235  frgra3vlem2  30593  3vfriswmgra  30597  frgraregorufr0  30645  2spotdisj  30654  nn0le2is012  30766  tpid3gVD  31578
  Copyright terms: Public domain W3C validator