Theorem 3mix3 1332

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 1330	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))
2		3orrot 1092	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
3	1, 2	sylib 217	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑))

Syntax hints:   → wi 4   ∨ w3o 1086

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 206  df-or 846  df-3or 1088

This theorem is referenced by:  3mix3i  1335  3mix3d  1338  3jaob  1426  tppreqb  4756  tpres  7136  onzsl  7764  sornom  10138  fpwwe2lem12  10503  nn0le2is012  12489  nn01to3  12786  qbtwnxr  13039  hash1to3  14309  swrdnd0  14468  pfxnd  14498  cshwshashlem1  16894  ostth  26892  nolesgn2o  26924  sltsolem1  26928  nosep2o  26935  btwncolinear1  34508  tpid3gVD  42835  limcicciooub  43566  dfxlim2v  43776