Theorem 3mix3 1331

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 1329	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))
2		3orrot 1091	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
3	1, 2	sylib 217	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 206  df-or 845  df-3or 1087

This theorem is referenced by:  3mix3i  1334  3mix3d  1337  3jaob  1425  tppreqb  4738  tpres  7076  onzsl  7693  sornom  10033  fpwwe2lem12  10398  nn0le2is012  12384  nn01to3  12681  qbtwnxr  12934  hash1to3  14205  swrdnd0  14370  pfxnd  14400  cshwshashlem1  16797  ostth  26787  nolesgn2o  33874  sltsolem1  33878  nosep2o  33885  btwncolinear1  34371  tpid3gVD  42462  limcicciooub  43178  dfxlim2v  43388