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

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

Proof of Theorem 3mix1
StepHypRef Expression
1 orc 399 . 2 (𝜑 → (𝜑 ∨ (𝜓𝜒)))
2 3orass 1034 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2sylibr 223 1 (𝜑 → (𝜑𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382   ∨ 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:  3mix2  1224  3mix3  1225  3mix1i  1226  3mix1d  1229  3jaob  1382  tppreqb  4277  onzsl  6938  sornom  8982  fpwwe2lem13  9343  hashv01gt1  12995  hash1to3  13128  cshwshashlem1  15640  zabsle1  24821  colinearalg  25590  frgraregorufr0  26579  sltsolem1  31067  frege129d  37074  frgrregorufr0  41489  nn0le2is012  41938
 Copyright terms: Public domain W3C validator