Theorem 3mix1 1349

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  3mix2  1350  3mix3  1351  3mix1i  1352  3mix1d  1355  tppreqb  4775  onzsl  7848  sornom  10276  fpwwe2lem12  10646  nn0le2is012  12680  hashv01gt1  14403  hash1to3  14551  cshwshashlem1  17181  zabsle1  27515  nogesgn1o  27892  ltssolem1  27894  nosep1o  27900  colinearalg  29319  frgrregorufr0  30750  frege129d  44566