Theorem 3mix3 1333

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

Syntax hints:   → wi 4   ∨ w3o 1085

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 207  df-or 848  df-3or 1087

This theorem is referenced by:  3mix3i  1336  3mix3d  1339  3jaobOLD  1429  tppreqb  4765  tpres  7157  onzsl  7802  sornom  10206  fpwwe2lem12  10571  nn0le2is012  12574  nn01to3  12876  qbtwnxr  13136  hash1to3  14433  swrdnd0  14598  pfxnd  14628  cshwshashlem1  17042  ostth  27583  nolesgn2o  27616  sltsolem1  27620  nosep2o  27627  btwncolinear1  36050  tpid3gVD  44824  limcicciooub  45628  dfxlim2v  45838