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 866 . 2 (𝜑 → (𝜑 ∨ (𝜓𝜒)))
2 3orass 1091 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2sylibr 233 1 (𝜑 → (𝜑𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846  w3o 1087
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 206  df-or 847  df-3or 1089
This theorem is referenced by:  3mix2  1332  3mix3  1333  3mix1i  1334  3mix1d  1337  3jaob  1427  tppreqb  4809  onzsl  7835  sornom  10272  fpwwe2lem12  10637  nn0le2is012  12626  hashv01gt1  14305  hash1to3  14452  cshwshashlem1  17029  zabsle1  26799  nogesgn1o  27176  sltsolem1  27178  nosep1o  27184  colinearalg  28168  frgrregorufr0  29577  frege129d  42514
  Copyright terms: Public domain W3C validator