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

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

Proof of Theorem 3mix1
StepHypRef Expression
1 orc 398 . 2 (𝜑 → (𝜑 ∨ (𝜓𝜒)))
2 3orass 1033 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2sylibr 222 1 (𝜑 → (𝜑𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381  w3o 1029
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 195  df-or 383  df-3or 1031
This theorem is referenced by:  3mix2  1223  3mix3  1224  3mix1i  1225  3mix1d  1228  3jaob  1381  tppreqb  4276  onzsl  6915  sornom  8959  fpwwe2lem13  9320  hashv01gt1  12947  hash1to3  13078  cshwshashlem1  15586  zabsle1  24738  colinearalg  25508  frgraregorufr0  26345  sltsolem1  30873  frege129d  36877  frgrregorufr0  41491  nn0le2is012  41940
  Copyright terms: Public domain W3C validator