Theorem 3mix3 1346

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

Syntax hints:   → wi 4   ∨ w3o 1097

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 209  df-or 859  df-3or 1099

This theorem is referenced by:  3mix3i  1349  3mix3d  1352  3jaobOLD  1446  tppreqb  4765  tpres  7185  onzsl  7826  sornom  10234  fpwwe2lem12  10600  nn0le2is012  12637  nn01to3  12942  qbtwnxr  13203  hash1to3  14505  swrdnd0  14671  pfxnd  14701  cshwshashlem1  17131  ostth  27703  nolesgn2o  27735  ltssolem1  27739  nosep2o  27746  btwncolinear1  36419  tpid3gVD  45417  limcicciooub  46211  dfxlim2v  46421