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

Theorem 3mix1 1157
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 385 . 2  |-  ( ph  ->  ( ph  \/  ( ps  \/  ch ) ) )
2 3orass 968 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
31, 2sylibr 212 1  |-  ( ph  ->  ( ph  \/  ps  \/  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    \/ w3o 964
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 966
This theorem is referenced by:  3mix2  1158  3mix3  1159  3mix1i  1160  3mix1d  1163  3jaob  1280  tppreqb  4019  onzsl  6462  elfiun  7685  sornom  8451  fpwwe2lem13  8814  hashv01gt1  12121  lsw0  12272  cshwshashlem1  14127  ostth  22893  colinearalg  23161  sltsolem1  27814  fnwe2lem3  29410  hash1to3  30240  frgraregorufr0  30650  nn0le2is012  30771
  Copyright terms: Public domain W3C validator