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

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

Proof of Theorem 3mix3
StepHypRef Expression
1 3mix1 1223 . 2 (𝜑 → (𝜑𝜓𝜒))
2 3orrot 1037 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
31, 2sylib 207 1 (𝜑 → (𝜓𝜒𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ w3o 1030 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 196  df-or 384  df-3or 1032 This theorem is referenced by:  3mix3i  1228  3mix3d  1231  3jaob  1382  tpid3gOLD  4249  tppreqb  4277  tpres  6371  onzsl  6938  sornom  8982  fpwwe2lem13  9343  nn01to3  11657  qbtwnxr  11905  hash1to3  13128  cshwshashlem1  15640  ostth  25128  sltsolem1  31067  btwncolinear1  31346  tpid3gVD  38099  limcicciooub  38704  pfxnd  40258  nn0le2is012  41938
 Copyright terms: Public domain W3C validator