Theorem 3mix3 1330

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

Syntax hints:   → wi 4   ∨ w3o 1084

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 844  df-3or 1086

This theorem is referenced by:  3mix3i  1333  3mix3d  1336  3jaob  1424  tppreqb  4807  tpres  7203  onzsl  7837  sornom  10274  fpwwe2lem12  10639  nn0le2is012  12630  nn01to3  12929  qbtwnxr  13183  hash1to3  14456  swrdnd0  14611  pfxnd  14641  cshwshashlem1  17033  ostth  27378  nolesgn2o  27410  sltsolem1  27414  nosep2o  27421  btwncolinear1  35345  tpid3gVD  43905  limcicciooub  44651  dfxlim2v  44861