Theorem 3mix1 1329

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

Syntax hints:   → wi 4   ∨ wo 847   ∨ w3o 1085

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 848  df-3or 1087

This theorem is referenced by:  3mix2  1330  3mix3  1331  3mix1i  1332  3mix1d  1335  3jaobOLD  1426  tppreqb  4809  onzsl  7866  sornom  10314  fpwwe2lem12  10679  nn0le2is012  12679  hashv01gt1  14380  hash1to3  14527  cshwshashlem1  17129  zabsle1  27354  nogesgn1o  27732  sltsolem1  27734  nosep1o  27740  colinearalg  28939  frgrregorufr0  30352  frege129d  43752