Theorem 3mix3 1330

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

Syntax hints:   → wi 4   ∨ w3o 1084

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

This theorem is referenced by:  3mix3i  1333  3mix3d  1336  3jaob  1424  tppreqb  4735  tpres  7058  onzsl  7668  sornom  9964  fpwwe2lem12  10329  nn0le2is012  12314  nn01to3  12610  qbtwnxr  12863  hash1to3  14133  swrdnd0  14298  pfxnd  14328  cshwshashlem1  16725  ostth  26692  nolesgn2o  33801  sltsolem1  33805  nosep2o  33812  btwncolinear1  34298  tpid3gVD  42351  limcicciooub  43068  dfxlim2v  43278