Theorem 3mix3 1349

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

Syntax hints:   → wi 4   ∨ w3o 1100

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 861  df-3or 1102

This theorem is referenced by:  3mix3i  1352  3mix3d  1355  tppreqb  4777  tpres  7200  onzsl  7842  sornom  10261  fpwwe2lem12  10627  nn0le2is012  12660  nn01to3  12965  qbtwnxr  13226  hash1to3  14529  swrdnd0  14695  pfxnd  14725  cshwshashlem1  17155  ostth  27769  nolesgn2o  27801  ltssolem1  27805  nosep2o  27812  btwncolinear1  36460  tpid3gVD  45442  limcicciooub  46243  dfxlim2v  46453