MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3mix3 Structured version   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  3911  tppreqb  3931  onzsl  4818  funtpg  5493  elfiun  7427  sornom  8149  fpwwe2lem13  8509  qbtwnxr  10778  hashv01gt1  11621  dyaddisjlem  19479  ostth  21325  spthispth  21565  3mix3d  25164  sltsolem1  25615  btwncolinear1  25995  fnwe2lem3  27118  cshwoor  28203  frgra3vlem2  28328  3vfriswmgra  28332  frgraregorufr0  28378  2spotdisj  28387  tpid3gVD  28891
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