Theorem 3mix3 1332

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

Syntax hints:   → wi 4   ∨ w3o 1086

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 847  df-3or 1088

This theorem is referenced by:  3mix3i  1335  3mix3d  1338  3jaobOLD  1427  tppreqb  4830  tpres  7238  onzsl  7883  sornom  10346  fpwwe2lem12  10711  nn0le2is012  12707  nn01to3  13006  qbtwnxr  13262  hash1to3  14541  swrdnd0  14705  pfxnd  14735  cshwshashlem1  17143  ostth  27701  nolesgn2o  27734  sltsolem1  27738  nosep2o  27745  btwncolinear1  36033  tpid3gVD  44813  limcicciooub  45558  dfxlim2v  45768