Theorem 3mix3 1351

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  3mix3i  1354  3mix3d  1357  tppreqb  4775  tpres  7206  onzsl  7848  sornom  10276  fpwwe2lem12  10644  nn0le2is012  12678  nn01to3  12983  qbtwnxr  13244  hash1to3  14549  swrdnd0  14719  pfxnd  14749  cshwshashlem1  17179  ostth  27856  nolesgn2o  27888  ltssolem1  27892  nosep2o  27899  btwncolinear1  36600  tpid3gVD  45610  limcicciooub  46411  dfxlim2v  46621