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

Theorem 3mix3 1168
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 1166 . 2  |-  ( ph  ->  ( ph  \/  ps  \/  ch ) )
2 3orrot 980 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )
31, 2sylib 196 1  |-  ( ph  ->  ( ps  \/  ch  \/  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 973
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 368  df-3or 975
This theorem is referenced by:  3mix3i  1171  3mix3d  1174  3jaob  1292  tpid3g  4087  tppreqb  4113  tpres  6104  onzsl  6664  sornom  8689  fpwwe2lem13  9050  nn01to3  11220  qbtwnxr  11452  hash1to3  12579  cshwshashlem1  14789  ostth  24205  sltsolem1  30128  btwncolinear1  30407  tpid3gVD  36672  limcicciooub  37011  pfxnd  37882  nn0le2is012  38467
  Copyright terms: Public domain W3C validator