Theorem 3mix3 1334

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 1332	. 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 849  df-3or 1088

This theorem is referenced by:  3mix3i  1337  3mix3d  1340  3jaobOLD  1430  tppreqb  4750  tpres  7156  onzsl  7797  sornom  10199  fpwwe2lem12  10565  nn0le2is012  12593  nn01to3  12891  qbtwnxr  13152  hash1to3  14454  swrdnd0  14620  pfxnd  14650  cshwshashlem1  17066  ostth  27602  nolesgn2o  27635  ltssolem1  27639  nosep2o  27646  btwncolinear1  36251  tpid3gVD  45268  limcicciooub  46065  dfxlim2v  46275