Theorem 3mix3 1329

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

Syntax hints:   → wi 4   ∨ w3o 1083

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 846  df-3or 1085

This theorem is referenced by:  3mix3i  1332  3mix3d  1335  3jaobOLD  1424  tppreqb  4814  tpres  7220  onzsl  7858  sornom  10322  fpwwe2lem12  10687  nn0le2is012  12680  nn01to3  12979  qbtwnxr  13235  hash1to3  14512  swrdnd0  14667  pfxnd  14697  cshwshashlem1  17100  ostth  27671  nolesgn2o  27704  sltsolem1  27708  nosep2o  27715  btwncolinear1  35895  tpid3gVD  44536  limcicciooub  45276  dfxlim2v  45486