Theorem 3mix1 1328

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

Syntax hints:   → wi 4   ∨ wo 843   ∨ w3o 1084

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 844  df-3or 1086

This theorem is referenced by:  3mix2  1329  3mix3  1330  3mix1i  1331  3mix1d  1334  3jaob  1424  tppreqb  4735  onzsl  7668  sornom  9964  fpwwe2lem12  10329  nn0le2is012  12314  hashv01gt1  13987  hash1to3  14133  cshwshashlem1  16725  zabsle1  26349  colinearalg  27181  frgrregorufr0  28589  nogesgn1o  33803  sltsolem1  33805  nosep1o  33811  frege129d  41260