Theorem 3mix1 1337

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

Syntax hints:   → wi 4   ∨ wo 853   ∨ w3o 1091

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 208  df-or 854  df-3or 1093

This theorem is referenced by:  3mix2  1338  3mix3  1339  3mix1i  1340  3mix1d  1343  3jaobOLD  1435  tppreqb  4739  onzsl  7787  sornom  10191  fpwwe2lem12  10557  nn0le2is012  12585  hashv01gt1  14299  hash1to3  14446  cshwshashlem1  17058  zabsle1  27278  nogesgn1o  27656  ltssolem1  27658  nosep1o  27664  colinearalg  28998  frgrregorufr0  30413  frege129d  44216