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

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

Proof of Theorem 3mix3
StepHypRef Expression
1 3mix1 1174 . 2  |-  ( ph  ->  ( ph  \/  ps  \/  ch ) )
2 3orrot 988 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )
31, 2sylib 199 1  |-  ( ph  ->  ( ps  \/  ch  \/  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 981
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 188  df-or 371  df-3or 983
This theorem is referenced by:  3mix3i  1179  3mix3d  1182  3jaob  1326  tpid3g  4115  tppreqb  4141  tpres  6132  onzsl  6687  sornom  8714  fpwwe2lem13  9074  nn01to3  11264  qbtwnxr  11500  hash1to3  12652  cshwshashlem1  15065  ostth  24475  sltsolem1  30562  btwncolinear1  30841  tpid3gVD  37211  limcicciooub  37657  pfxnd  38806  nn0le2is012  39770
  Copyright terms: Public domain W3C validator