Theorem 3mix1 1326

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

Syntax hints:   → wi 4   ∨ wo 843   ∨ w3o 1082

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 844  df-3or 1084

This theorem is referenced by:  3mix2  1327  3mix3  1328  3mix1i  1329  3mix1d  1332  3jaob  1422  tppreqb  4738  onzsl  7561  sornom  9699  fpwwe2lem13  10064  nn0le2is012  12047  hashv01gt1  13706  hash1to3  13850  cshwshashlem1  16429  zabsle1  25872  colinearalg  26696  frgrregorufr0  28103  sltsolem1  33180  nosep1o  33186  frege129d  40128