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

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

Proof of Theorem 3mix1
StepHypRef Expression
1 orc 376 . 2  |-  ( ph  ->  ( ph  \/  ( ps  \/  ch ) ) )
2 3orass 940 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
31, 2sylibr 205 1  |-  ( ph  ->  ( ph  \/  ps  \/  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359    \/ w3o 936
This theorem is referenced by:  3mix2  1128  3mix3  1129  3mix1i  1130  3jaob  1247  tppreqb  3941  onzsl  4828  elfiun  7437  sornom  8159  fpwwe2lem13  8519  hashv01gt1  11631  ostth  21335  3mix1d  25172  sltsolem1  25625  colinearalg  25851  fnwe2lem3  27129  lswrd0  28283  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