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

Theorem 3mix3 1432
Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
Assertion
Ref Expression
3mix3 (𝜑 → (𝜓𝜒𝜑))

Proof of Theorem 3mix3
StepHypRef Expression
1 3mix1 1430 . 2 (𝜑 → (𝜑𝜓𝜒))
2 3orrot 1113 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
31, 2sylib 210 1 (𝜑 → (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1107
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 199  df-or 875  df-3or 1109
This theorem is referenced by:  3mix3i  1435  3mix3d  1438  3jaob  1552  tppreqb  4524  tpres  6695  onzsl  7280  sornom  9387  fpwwe2lem13  9752  nn0le2is012  11731  nn01to3  12026  qbtwnxr  12280  hash1to3  13522  swrdnd0  13686  pfxnd  13730  cshwshashlem1  16130  ostth  25680  nolesgn2o  32337  sltsolem1  32339  btwncolinear1  32689  tpid3gVD  39838  limcicciooub  40613  dfxlim2v  40817
  Copyright terms: Public domain W3C validator