Theorem 3mix1 1345

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

Syntax hints:   → wi 4   ∨ wo 858   ∨ w3o 1098

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 209  df-or 859  df-3or 1100

This theorem is referenced by:  3mix2  1346  3mix3  1347  3mix1i  1348  3mix1d  1351  3jaobOLD  1447  tppreqb  4766  onzsl  7827  sornom  10235  fpwwe2lem12  10601  nn0le2is012  12638  hashv01gt1  14359  hash1to3  14506  cshwshashlem1  17132  zabsle1  27361  nogesgn1o  27738  ltssolem1  27740  nosep1o  27746  colinearalg  29112  frgrregorufr0  30527  frege129d  44340