Theorem 3mix3 1339

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

Syntax hints:   → wi 4   ∨ w3o 1091

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 208  df-or 854  df-3or 1093

This theorem is referenced by:  3mix3i  1342  3mix3d  1345  3jaobOLD  1435  tppreqb  4738  tpres  7145  onzsl  7786  sornom  10190  fpwwe2lem12  10556  nn0le2is012  12584  nn01to3  12882  qbtwnxr  13143  hash1to3  14445  swrdnd0  14611  pfxnd  14641  cshwshashlem1  17057  ostth  27620  nolesgn2o  27653  ltssolem1  27657  nosep2o  27664  btwncolinear1  36297  tpid3gVD  45285  limcicciooub  46080  dfxlim2v  46290