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

Theorem 3mix1 1165
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 976 . 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 972
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 974
This theorem is referenced by:  3mix2  1166  3mix3  1167  3mix1i  1168  3mix1d  1171  3jaob  1290  tppreqb  4174  onzsl  6676  sornom  8669  fpwwe2lem13  9032  hashv01gt1  12398  hash1to3  12510  cshwshashlem1  14454  colinearalg  24045  frgraregorufr0  24884  sltsolem1  29362  nn0le2is012  32441
  Copyright terms: Public domain W3C validator