Theorem 3mix1 1332

Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Assertion

Ref	Expression
3mix1	⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))

Proof of Theorem 3mix1

Step	Hyp	Ref	Expression
1		orc 868	. 2 ⊢ (𝜑 → (𝜑 ∨ (𝜓 ∨ 𝜒)))
2		3orass 1090	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	sylibr 234	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))

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  1333  3mix3  1334  3mix1i  1335  3mix1d  1338  3jaobOLD  1430  tppreqb  4749  onzsl  7790  sornom  10190  fpwwe2lem12  10556  nn0le2is012  12584  hashv01gt1  14298  hash1to3  14445  cshwshashlem1  17057  zabsle1  27273  nogesgn1o  27651  ltssolem1  27653  nosep1o  27659  colinearalg  28993  frgrregorufr0  30409  frege129d  44208