Theorem 3mix1 1415

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

Syntax hints:   → wi 4   ∨ wo 382   ∨ w3o 1071

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 197  df-or 384  df-3or 1073

This theorem is referenced by:  3mix2  1416  3mix3  1417  3mix1i  1418  3mix1d  1421  3jaob  1539  tppreqb  4481  onzsl  7212  sornom  9311  fpwwe2lem13  9676  nn0le2is012  11653  hashv01gt1  13347  hash1to3  13485  cshwshashlem1  16024  zabsle1  25241  colinearalg  26010  frgrregorufr0  27499  sltsolem1  32153  nosep1o  32159  frege129d  38575