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

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

Proof of Theorem 3mix2
StepHypRef Expression
1 3mix1 1165 . 2  |-  ( ph  ->  ( ph  \/  ch  \/  ps ) )
2 3orrot 979 . 2  |-  ( ( ps  \/  ph  \/  ch )  <->  ( ph  \/  ch  \/  ps ) )
31, 2sylibr 212 1  |-  ( ph  ->  ( ps  \/  ph  \/  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 972
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
This theorem is referenced by:  3mix2i  1169  3mix2d  1172  3jaob  1290  tppreqb  4168  sosn  5069  funtpg  5638  onzsl  6665  elfiun  7890  sornom  8657  fpwwe2lem13  9020  hash1to3  12496  cshwshashlem1  14438  dyaddisjlem  21767  ostth  23580  frgraregorufr0  24757  sltsolem1  29033  nodenselem8  29053  fnwe2lem3  30630  icccncfext  31254  nn0le2is012  32053
  Copyright terms: Public domain W3C validator