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

Theorem 3mix2 1128
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 1127 . 2  |-  ( ph  ->  ( ph  \/  ch  \/  ps ) )
2 3orrot 943 . 2  |-  ( ( ps  \/  ph  \/  ch )  <->  ( ph  \/  ch  \/  ps ) )
31, 2sylibr 205 1  |-  ( ph  ->  ( ps  \/  ph  \/  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 936
This theorem is referenced by:  3mix2i  1131  3jaob  1247  tppreqb  3941  onzsl  4828  sosn  4949  funtpg  5503  elfiun  7437  sornom  8159  fpwwe2lem13  8519  dyaddisjlem  19489  ostth  21335  3mix2d  25173  sltsolem1  25625  nodenselem8  25645  fnwe2lem3  27129  swrd0  28205  cshwoor  28259  frgraregorufr0  28503
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 179  df-or 361  df-3or 938
  Copyright terms: Public domain W3C validator