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

Theorem 3mix2 1158
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 1157 . 2  |-  ( ph  ->  ( ph  \/  ch  \/  ps ) )
2 3orrot 971 . 2  |-  ( ( ps  \/  ph  \/  ch )  <->  ( ph  \/  ch  \/  ps ) )
31, 2sylibr 212 1  |-  ( ph  ->  ( ps  \/  ph  \/  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ 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:  3mix2i  1161  3mix2d  1164  3jaob  1280  tppreqb  4019  sosn  4913  funtpg  5473  onzsl  6462  elfiun  7685  sornom  8451  fpwwe2lem13  8814  cshwshashlem1  14127  dyaddisjlem  21080  ostth  22893  sltsolem1  27814  nodenselem8  27834  fnwe2lem3  29410  hash1to3  30240  frgraregorufr0  30650  nn0le2is012  30771
  Copyright terms: Public domain W3C validator