Theorem 3mix1 1331

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 866	. 2 ⊢ (𝜑 → (𝜑 ∨ (𝜓 ∨ 𝜒)))
2		3orass 1091	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	sylibr 233	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))

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  4806  onzsl  7829  sornom  10267  fpwwe2lem12  10632  nn0le2is012  12621  hashv01gt1  14300  hash1to3  14447  cshwshashlem1  17024  zabsle1  26778  nogesgn1o  27155  sltsolem1  27157  nosep1o  27163  colinearalg  28147  frgrregorufr0  29556  frege129d  42446