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

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

Proof of Theorem 3mix1
StepHypRef Expression
1 orc 868 . 2 (𝜑 → (𝜑 ∨ (𝜓𝜒)))
2 3orass 1090 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2sylibr 234 1 (𝜑 → (𝜑𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 848  w3o 1086
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 207  df-or 849  df-3or 1088
This theorem is referenced by:  3mix2  1332  3mix3  1333  3mix1i  1334  3mix1d  1337  3jaobOLD  1429  tppreqb  4805  onzsl  7867  sornom  10317  fpwwe2lem12  10682  nn0le2is012  12682  hashv01gt1  14384  hash1to3  14531  cshwshashlem1  17133  zabsle1  27340  nogesgn1o  27718  sltsolem1  27720  nosep1o  27726  colinearalg  28925  frgrregorufr0  30343  frege129d  43776
  Copyright terms: Public domain W3C validator