Theorem 3mix1 1347

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

Syntax hints:   → wi 4   ∨ wo 860   ∨ w3o 1100

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 210  df-or 861  df-3or 1102

This theorem is referenced by:  3mix2  1348  3mix3  1349  3mix1i  1350  3mix1d  1353  tppreqb  4777  onzsl  7842  sornom  10261  fpwwe2lem12  10627  nn0le2is012  12660  hashv01gt1  14381  hash1to3  14529  cshwshashlem1  17155  zabsle1  27426  nogesgn1o  27803  ltssolem1  27805  nosep1o  27811  colinearalg  29201  frgrregorufr0  30616  frege129d  44415