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

Theorem 3mix3 1167
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 1165 . 2  |-  ( ph  ->  ( ph  \/  ps  \/  ch ) )
2 3orrot 979 . 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 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:  3mix3i  1170  3mix3d  1173  3jaob  1290  tpid3g  4142  tppreqb  4168  funtpg  5636  onzsl  6659  elfiun  7886  sornom  8653  fpwwe2lem13  9016  nn01to3  11171  qbtwnxr  11395  hashv01gt1  12380  hash1to3  12490  cshwshashlem1  14431  dyaddisjlem  21736  ostth  23549  spthispth  24248  frgra3vlem2  24674  3vfriswmgra  24678  frgraregorufr0  24726  2spotdisj  24735  sltsolem1  29002  btwncolinear1  29293  fnwe2lem3  30602  limcicciooub  31179  nn0le2is012  32021  tpid3gVD  32722
  Copyright terms: Public domain W3C validator