Theorem 3mix3 1329

Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Assertion

Ref	Expression
3mix3	⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑))

Proof of Theorem 3mix3

Step	Hyp	Ref	Expression
1		3mix1 1327	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))
2		3orrot 1089	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
3	1, 2	sylib 221	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑))

Syntax hints:   → wi 4   ∨ w3o 1083

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 845  df-3or 1085

This theorem is referenced by:  3mix3i  1332  3mix3d  1335  3jaob  1423  tppreqb  4698  tpres  6940  onzsl  7541  sornom  9688  fpwwe2lem13  10053  nn0le2is012  12034  nn01to3  12329  qbtwnxr  12581  hash1to3  13845  swrdnd0  14010  pfxnd  14040  cshwshashlem1  16421  ostth  26223  nolesgn2o  33291  sltsolem1  33293  btwncolinear1  33643  tpid3gVD  41548  limcicciooub  42279  dfxlim2v  42489