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 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑))

Syntax hints:   → wi 4   ∨ w3o 1102

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 1104

This theorem is referenced by:  3mix3i  1354  3mix3d  1357  tppreqb  4773  tpres  7199  onzsl  7838  sornom  10256  fpwwe2lem12  10622  nn0le2is012  12655  nn01to3  12960  qbtwnxr  13221  hash1to3  14525  swrdnd0  14691  pfxnd  14721  cshwshashlem1  17150  ostth  27803  nolesgn2o  27835  ltssolem1  27839  nosep2o  27846  btwncolinear1  36561  tpid3gVD  45570  limcicciooub  46371  dfxlim2v  46581