Theorem 3mix3 1417

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

Syntax hints:   → wi 4   ∨ 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:  3mix3i  1420  3mix3d  1423  3jaob  1539  tppreqb  4481  tpres  6630  onzsl  7211  sornom  9291  fpwwe2lem13  9656  nn0le2is012  11633  nn01to3  11974  qbtwnxr  12224  hash1to3  13465  cshwshashlem1  16004  ostth  25527  nolesgn2o  32130  sltsolem1  32132  btwncolinear1  32482  tpid3gVD  39576  limcicciooub  40372  dfxlim2v  40576  pfxnd  41905