Theorem 3mix3 1333

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 1331	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))
2		3orrot 1092	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
3	1, 2	sylib 218	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 207  df-or 849  df-3or 1088

This theorem is referenced by:  3mix3i  1336  3mix3d  1339  3jaobOLD  1429  tppreqb  4805  tpres  7221  onzsl  7867  sornom  10317  fpwwe2lem12  10682  nn0le2is012  12682  nn01to3  12983  qbtwnxr  13242  hash1to3  14531  swrdnd0  14695  pfxnd  14725  cshwshashlem1  17133  ostth  27683  nolesgn2o  27716  sltsolem1  27720  nosep2o  27727  btwncolinear1  36070  tpid3gVD  44862  limcicciooub  45652  dfxlim2v  45862