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

Theorem 3mix1 1415
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 1075 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2sylibr 224 1 (𝜑 → (𝜑𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  w3o 1071
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 197  df-or 384  df-3or 1073
This theorem is referenced by:  3mix2  1416  3mix3  1417  3mix1i  1418  3mix1d  1421  3jaob  1539  tppreqb  4481  onzsl  7211  sornom  9291  fpwwe2lem13  9656  nn0le2is012  11633  hashv01gt1  13327  hash1to3  13465  cshwshashlem1  16004  zabsle1  25220  colinearalg  25989  frgrregorufr0  27478  sltsolem1  32132  nosep1o  32138  frege129d  38557
  Copyright terms: Public domain W3C validator