Theorem 3mix3 1432

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

Syntax hints:   → wi 4   ∨ w3o 1107

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 199  df-or 875  df-3or 1109

This theorem is referenced by:  3mix3i  1435  3mix3d  1438  3jaob  1552  tppreqb  4524  tpres  6695  onzsl  7280  sornom  9387  fpwwe2lem13  9752  nn0le2is012  11731  nn01to3  12026  qbtwnxr  12280  hash1to3  13522  swrdnd0  13686  pfxnd  13730  cshwshashlem1  16130  ostth  25680  nolesgn2o  32337  sltsolem1  32339  btwncolinear1  32689  tpid3gVD  39838  limcicciooub  40613  dfxlim2v  40817