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

Theorem 3mix2 1125
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 1124 . 2  |-  ( ph  ->  ( ph  \/  ch  \/  ps ) )
2 3orrot 940 . 2  |-  ( ( ps  \/  ph  \/  ch )  <->  ( ph  \/  ch  \/  ps ) )
31, 2sylibr 203 1  |-  ( ph  ->  ( ps  \/  ph  \/  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 933
This theorem is referenced by:  3mix2i  1128  3jaob  1244  onzsl  4637  sosn  4759  elfiun  7183  sornom  7903  fpwwe2lem13  8264  dyaddisjlem  18950  ostth  20788  3mix2d  24068  sltsolem1  24322  nodenselem8  24342  sgplpte21d1  26139  xsyysx  26145  fnwe2lem3  27149
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