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

Theorem 3mix1 1124
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 374 . 2  |-  ( ph  ->  ( ph  \/  ( ps  \/  ch ) ) )
2 3orass 937 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
31, 2sylibr 203 1  |-  ( ph  ->  ( ph  \/  ps  \/  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    \/ w3o 933
This theorem is referenced by:  3mix2  1125  3mix3  1126  3mix1i  1127  3jaob  1244  onzsl  4637  elfiun  7183  sornom  7903  fpwwe2lem13  8264  ostth  20788  3mix1d  23478  sltsolem1  23733  colinearalg  23949  pxysxy  25554  fnwe2lem3  26561
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