Theorem 3mix3 1328

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

Syntax hints:   → wi 4   ∨ w3o 1082

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 209  df-or 844  df-3or 1084

This theorem is referenced by:  3mix3i  1331  3mix3d  1334  3jaob  1422  tppreqb  4738  tpres  6963  onzsl  7561  sornom  9699  fpwwe2lem13  10064  nn0le2is012  12047  nn01to3  12342  qbtwnxr  12594  hash1to3  13850  swrdnd0  14019  pfxnd  14049  cshwshashlem1  16429  ostth  26215  nolesgn2o  33178  sltsolem1  33180  btwncolinear1  33530  tpid3gVD  41196  limcicciooub  41938  dfxlim2v  42148